1. T : Type
2. Q : (T List)Prop
3. Q(nil)
4. ys:T List, x:T. Q(ys)  Q(ys @ [x])
5. n:, l:T List. ||l|| = n  Q(l)
  zs:T List. Q(zs)

By:	Auto THEN AllHyps (i.InstHyp [||zs||;zs] i THENA Complete Auto) THEN Trivial

None

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