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
  (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)))

By:	Guarding (R(a,x,<arg>)  R(a,x,<arg>)) Auto

1

5. a : A 6. 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))

1 step

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