IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card st vs msize1111 1. a : 2. P : aProp
3. f : a2
4. i:a. P(i) f(i) = 1
5. x : a 6. P(x)
0 (f(x))
By:
FwdThru: Hyp:4 on [ P(x) ]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
i:
f(i) = 1
0 
