IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
l exists nil T:Type, P:(TProp). (xnil.P(x)) False
By:
Unfold `l_exists` 0 THEN ExRepD THEN RWO Thm*x:T. (x nil) False -2
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
T:Type, P:(T
Prop). (
x
nil.P(x)) 
False
