Nuprl - Proof: decidable ex unit 1

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 1

1. P : Unit

Prop
2. Dec(P(

))
3. x : Unit

Dec(P(x))

By:	Analyze -1 THEN Fold `it` 0

Generated subgoals:

None

About:

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