DEFINITION aprem_ind()
TYPE =
       ∀P:nat→A→A→Prop
         .∀a:A.∀a1:A.(P O (AHead a a1) a)
           →(∀a:A.∀a1:A.∀n:nat.(aprem n a a1)→(P n a a1)→∀a2:A.(P (S n) (AHead a2 a) a1)
                →∀n:nat.∀a:A.∀a1:A.(aprem n a a1)→(P n a a1))
BODY =
        assume P: nat→A→A→Prop
        suppose H: ∀a:A.∀a1:A.(P O (AHead a a1) a)
        suppose H1: ∀a:A.∀a1:A.∀n:nat.(aprem n a a1)→(P n a a1)→∀a2:A.(P (S n) (AHead a2 a) a1)
          (aux) by well-founded reasoning we prove ∀n:nat.∀a:A.∀a1:A.(aprem n a a1)→(P n a a1)
           assume n: nat
           assume a: A
           assume a1: A
           suppose H2: aprem n a a1
             by cases on H2 we prove P n a a1
                case aprem_zero a2:A a3:A ⇒
                   the thesis becomes P O (AHead a2 a3) a2
                   by (H . .)
P O (AHead a2 a3) a2
                case aprem_succ a2:A a3:A n1:nat H3:aprem n1 a2 a3 a4:A ⇒
                   the thesis becomes P (S n1) (AHead a4 a2) a3
                   by (aux . . . H3)
                   we proved P n1 a2 a3
                   by (H1 . . . H3 previous .)
P (S n1) (AHead a4 a2) a3
             we proved P n a a1
∀n:nat.∀a:A.∀a1:A.(aprem n a a1)→(P n a a1)
          done
          consider aux
          we proved ∀n:nat.∀a:A.∀a1:A.(aprem n a a1)→(P n a a1)
       we proved 
          ∀P:nat→A→A→Prop
            .∀a:A.∀a1:A.(P O (AHead a a1) a)
              →(∀a:A.∀a1:A.∀n:nat.(aprem n a a1)→(P n a a1)→∀a2:A.(P (S n) (AHead a2 a) a1)
                   →∀n:nat.∀a:A.∀a1:A.(aprem n a a1)→(P n a a1))