DEFINITION aprem_asucc()
TYPE =
       ∀g:G.∀a1:A.∀a2:A.∀i:nat.(aprem i a1 a2)→(aprem i (asucc g a1) a2)
BODY =
        assume g: G
        assume a1: A
        assume a2: A
        assume i: nat
        suppose H: aprem i a1 a2
          we proceed by induction on H to prove aprem i (asucc g a1) a2
             case aprem_zero : a0:A a3:A ⇒
                the thesis becomes aprem O (asucc g (AHead a0 a3)) a0
                   by (aprem_zero . .)
                   we proved aprem O (AHead a0 (asucc g a3)) a0
aprem O (asucc g (AHead a0 a3)) a0
             case aprem_succ : a0:A a:A i0:nat :aprem i0 a0 a a3:A ⇒
                the thesis becomes aprem (S i0) (asucc g (AHead a3 a0)) a
                (H1) by induction hypothesis we know aprem i0 (asucc g a0) a
                   by (aprem_succ . . . H1 .)
                   we proved aprem (S i0) (AHead a3 (asucc g a0)) a
aprem (S i0) (asucc g (AHead a3 a0)) a
          we proved aprem i (asucc g a1) a2
       we proved ∀g:G.∀a1:A.∀a2:A.∀i:nat.(aprem i a1 a2)→(aprem i (asucc g a1) a2)