(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 2 1 1 2
1. T : Type
2. Q : (T List)Prop
3. Q(nil)
4. ys:T List, x:T. Q(ys)  Q(ys @ [x])
5. n : 
6. 0<n
7. l:T List. ||l|| = n-1  Q(l)
8. l : T List
9. x : T
10. L' : T List
11. l = (L' @ [x])
  ||L'||+1 = n    Q(L' @ [x])
By: Auto THEN AllHyps (i.BackThru i THEN Complete (Auto THEN BackThruSomeHyp))

Generated subgoals:

None

About:
listconsnilintnatural_numberaddsubtractless_than
functionuniverseequalpropimpliesall
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