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

None

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