(10steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: list append singleton ind 1 1 1
1. T : Type
2. Q : (T List)Prop
3. Q(nil)
4. ys:T List, x:T. Q(ys)  Q(ys @ [x])
  l:T List. ||l|| = 0    Q(l)
By: Auto THEN Subst (l = nil) 0
THEN
BackThru Thm* l:T List. ||l|| = 0    l = nil

Generated subgoals:

None

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

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