(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. T : Type
2. Q : (T List)Prop
3. Q(nil)
4. ys:T List, x:TQ(ys Q(ys @ [x])
  zs:T List. Q(zs)


By: Assert (n:l:T List. ||l|| = n  Q(l))


Generated subgoals:

1   n:l:T List. ||l|| = n    Q(l)
7 steps
2 5. n:l:T List. ||l|| = n    Q(l)
  zs:T List. Q(zs)

1 step

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