IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable-exists-finite112 1. T : Type
2. P : TProp
3. x:T. Dec(P(x))
4. n : 5. f : nT 6. b:T. a:n. f(a) = b 7. i : n 8. P(f(i))
x:T. P(x)
By:
InstConcl [f(i)]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
x:T. Dec(P(x))
a:
