(6steps total) PrintForm Definitions mb list 1 Sections MarkB generic Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: append is nil
  T:Type, l1,l2:T List. (l1 @ l2) = nil  l1 = nil & l2 = nil
By: Assert (T:Type, x:T, l:T List. [x / l] = nil  False)

Generated subgoals:

1   T:Type, x:T, l:T List. [x / l] = nil  False
3 steps
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
2 steps

About:
listconsniluniverseequalimpliesandfalseall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

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