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 =
        assume A: Set
        assume R: A→A→Prop
        assume P: A→Prop
        suppose H: ∀a:A.(∀y:A.(R y a)→(Acc A R y))→(∀a1:A.(R a1 a)→(P a1))→(P a)
          (aux) by well-founded reasoning we prove ∀a:A.(Acc A R a)→(P a)
           assume a: A
           suppose H1: Acc A R a
             by cases on H1 we prove P a
                case Acc_intro a1:A H2:∀y:A.(R y a1)→(Acc A R y) ⇒
                   the thesis becomes P a1
                    assume a2: A
                    suppose H3: R a2 a1
                      by (H2 . H3)
                      we proved Acc A R a2
                      by (aux . previous)
                      we proved P a2
                   we proved ∀a2:A.(R a2 a1)→(P a2)
                   by (H . H2 previous)
P a1
             we proved P a
∀a:A.(Acc A R a)→(P a)
          done
          consider aux
          we proved ∀a:A.(Acc A R a)→(P a)
       we proved 
          ∀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)