PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /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:
nilfunctionuniversepropfalseall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc