IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
l all nil T:Type, P:(TProp). (xnil.P(x))
By:
Unfold `l_all` 0 THEN Unfold `l_member` 0 THEN Reduce 0 THEN ExRepD
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html