DEFINITION aplus_reg_r()
TYPE =
       ∀g:G
         .∀a1:A
           .∀a2:A
             .∀h1:nat
               .∀h2:nat
                 .eq A (aplus g a1 h1) (aplus g a2 h2)
                   →∀h:nat.(eq A (aplus g a1 (plus h h1)) (aplus g a2 (plus h h2)))
BODY =
        assume g: G
        assume a1: A
        assume a2: A
        assume h1: nat
        assume h2: nat
        suppose H: eq A (aplus g a1 h1) (aplus g a2 h2)
        assume h: nat
          we proceed by induction on h to prove eq A (aplus g a1 (plus h h1)) (aplus g a2 (plus h h2))
             case O : ⇒
                the thesis becomes eq A (aplus g a1 (plus O h1)) (aplus g a2 (plus O h2))
                   consider H
                   we proved eq A (aplus g a1 h1) (aplus g a2 h2)
eq A (aplus g a1 (plus O h1)) (aplus g a2 (plus O h2))
             case S : n:nat ⇒
                the thesis becomes eq A (aplus g a1 (plus (S n) h1)) (aplus g a2 (plus (S n) h2))
                (H0) by induction hypothesis we know eq A (aplus g a1 (plus n h1)) (aplus g a2 (plus n h2))
                   by (refl_equal . .)
                   we proved eq G g g
                   by (f_equal2 . . . . . . . . previous H0)
                   we proved 
                      eq
                        A
                        asucc g (aplus g a1 (plus n h1))
                        asucc g (aplus g a2 (plus n h2))
eq A (aplus g a1 (plus (S n) h1)) (aplus g a2 (plus (S n) h2))
          we proved eq A (aplus g a1 (plus h h1)) (aplus g a2 (plus h h2))
       we proved 
          ∀g:G
            .∀a1:A
              .∀a2:A
                .∀h1:nat
                  .∀h2:nat
                    .eq A (aplus g a1 h1) (aplus g a2 h2)
                      →∀h:nat.(eq A (aplus g a1 (plus h h1)) (aplus g a2 (plus h h2)))