DEFINITION Acc_ind()
TYPE =
       ∀A:Set
         .∀R:A→A→Prop
           .∀P:A→Prop
             .∀a:A.(∀y:A.(R y a)→(Acc A R y))→(∀a1:A.(R a1 a)→(P a1))→(P a)
               →∀a:A.(Acc A R a)→(P a)
BODY =
Show proof