Nuprl - Proof: decidable ex unit

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable ex unit

P:(Unit

Prop). Dec(P(

))

Dec(

x:Unit. P(x))

By:	Auto THEN BackThru Thm* P:(TProp). (x:T. Dec(P(x))) finite-type(T) Dec(x:T. P(x))

Generated subgoals:

1 1. P : UnitProp
2. Dec(P())
3. x : Unit
Dec(P(x))
1 step

2 1. P : UnitProp
2. Dec(P())
finite-type(Unit)
3 steps

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

1	1. P : UnitProp 2. Dec(P()) 3. x : Unit Dec(P(x))	1 step
2	1. P : UnitProp 2. Dec(P()) finite-type(Unit)	3 steps