(6steps total) PrintForm Definitions hol list 2 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: not nil cons2 1

1. 'a : S
2. t : 'a List
3. h : 'a
  nil = cons(ht False


By: Analyze 0


Generated subgoals:

1   nil = cons(ht False
3 steps
2   (nil = cons(ht))  False
Auto

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

(6steps total) PrintForm Definitions hol list 2 Sections HOLlib Doc