A:Type, Q:Prop, 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)))

1

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

5 steps

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