(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
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' @ [x]|| = n    Q(L' @ [x])
By: Subst (||L' @ [x]|| = ||L'||+1) 0

Generated subgoals:

1   ||L' @ [x]|| = ||L'||+1  
1 step
2   ||L'||+1 = n    Q(L' @ [x])
1 step

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