1. A : Type
2. Q : Prop
3. R : A(A List)PropProp
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)))

1

(Q  Q)   & (a:A, x:A List.   & (R(a,x,Case of 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)))

2 steps

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