IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable-exists-finite12 1. T : Type
2. P : TProp
3. x:T. Dec(P(x))
4. n : 5. f : nT 6. Surj(n; T; f)
7. (x:T. P(x)) (i:n. P(f(i)))
Dec(x:T. P(x))
By:
RW (SweepDnC (HypC -1)) 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
x:T. Dec(P(x))
x:T. P(x)) 
(
Dec(
