IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
l all cons31 1. T : Type
2. P : TProp
3. x : T 4. L : T List
5. P(x)
6. y:T. (yL) P(y)
7. y : T 8. y = x P(y)
By:
HypSubst -1 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
y:T. (y 
L) 
P(y)
P(y)
