IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
assert of null1 1. T : Type
2. T List
3. u : T 4. v : T List
5. u.v = nil
False
By:
MoveToConcl 5 THEN Fold `not` 0 THEN BackThru Thm*h:T, t:T List. h.t = nil
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html