Nuprl - Proof: list append singleton ind 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: list append singleton ind 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|| = n

Q(l)

By:	Analyze 0 THEN NatInd -1

Generated subgoals:

1   l:T List. ||l|| = 0    Q(l)
1 step

2 5. n :
6. 0<n
7. l:T List. ||l|| = n-1    Q(l)
  l:T List. ||l|| = n    Q(l)
5 steps

About:

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

1	l:T List. \|\|l\|\| = 0 Q(l)	1 step
2	5. n : 6. 0<n 7. l:T List. \|\|l\|\| = n-1 Q(l) l:T List. \|\|l\|\| = n Q(l)	5 steps