IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
least exists1111 1. k : 2. P : kProp
3. i:k. P(i)
4. p : k 5. i:k. p(i) P(i)
i:k. p(i)
By:
Rewrite by Hyp:5
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
i:
i:
P(i)
