(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 1
  T:Type, x:T, l:T List. [x / l] = nil  False
By: Auto THEN ApFunToHypEquands `z' ||z||  -1

Generated subgoal:

1 1. T : Type
2. x : T
3. l : T List
4. [x / l] = nil
5. ||[x / l]|| = ||nil||  
  False
2 steps

About:
listconsniluniverseequalimpliesfalseall
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