IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
member exists T:Type, L:T List. L = nil (x:T. (xL))
By:
Unfold `l_member` 0 THEN AssertBY (0<||L||) Easy THEN InstConcl [L[0];0]
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, L:T List. 
L = nil 
(
x:T. (x 
L))
