IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
l exists cons12 1. T : Type
2. P : TProp
3. T 4. L : T List
5. y : T 6. (yL)
7. P(y)
y:T. (yL) & P(y)
By:
AutoInstConcl []
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html