(6steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: append is nil 2
1. T:Type, x:T, l:T List. [x / l] = nil  False
  T:Type, l1,l2:T List. (l1 @ l2) = nil  l1 = nil & l2 = nil
By: ((Analyze 0) THEN (Analyze 0)) THEN ListInd -1 THEN Reduce 0
THEN
Try (Complete Auto)

Generated subgoal:

1 2. T : Type
3. T List
4. u : T
5. v : T List
6. l2:T List. (v @ l2) = nil  v = nil & l2 = nil
  l2:T List. [u / (v @ l2)] = nil  [u / v] = nil & l2 = nil
1 step

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

(6steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc