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

{p:(A

x:A. p(x)

P(x) }

By:

Analyze

Generated subgoal:

1 f = g
2 steps

About:

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