IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
l all cons2 1. T : Type
2. P : TProp
3. x : T 4. L : T List
5. y:T. (y [x / L]) P(y)
6. y : T 7. (yL)
P(y)
By:
BackThruSomeHyp
THEN
RWO Thm*l:T List, a,x:T. (x [a / l]) x = a (xl) 0
THEN
SimpConcl
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html