Nuprl - Proof: dec pred imp bool decider exists 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: dec pred imp bool decider exists 1 1

1. A : Type
2. P : A

Type
3.

x:A. Dec(P(x))
4. f : A

x:A. f(x)

P(x)
6. g : A

x:A. g(x)

P(x)

f = g

{p:(A

x:A. p(x)

P(x) }

By:	Rewrite-3 by Hyp:-1

Generated subgoal:

1 8. x:A. f(x) g(x)
f = g {p:(A)| x:A. p(x) P(x) }
3 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html