1. A : Type
2. Q : Prop
3. R : A(A List)PropProp
  P:((A List)Prop). (P(nil)  Q) & (a:A, x:A List. P(a.x)  R(a,x,P(x)))

By:	Witness: x.Case of x; nil  Q ; a.x, rec:r  R(a,x,r) with type (A List)Prop THEN ReduceSOAps Concl

1	4. x : A List   (Case of x; nil  Q ; a.x, rec:r  R(a,x,r))  Prop	1 step
2	4. (x.Case of x; nil  Q ; a.x, rec:r  R(a,x,r))  (A List)Prop   ((Case of nil; nil  Q ; a.x, rec:r  R(a,x,r))  Q)   & (a:A, x:A List.   & ((Case of a.x; nil  Q ; a.x, rec:r  R(a,x,r))   & (   & (R(a,x,Case of x; nil  Q ; a.x, rec:r  R(a,x,r)))	3 steps

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