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 =
Show proof