Nuprl - Proof: dec pred imp bool decider exists 1 1 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 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)
8.

x:A. f(x)

g(x)

f = g

By:	FunExtensionality

Generated subgoal:

1 9. x : A
f(x) = g(x)
1 step

About:

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