(2steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: assert of null 1

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:Tt:T List. h.t = nil


Generated subgoals:

None

About:
listconsniluniverseequalfalseall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(2steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc