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

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)
9. x : A

f(x) = g(x)

By:	BackThru: Thm* a,b:. (a b) a = b THEN Inst: Hyp:8 Using:[x]

Generated subgoals:

None

About:

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