DEFINITION aplus_assoc()
TYPE =
       ∀g:G.∀a:A.∀h1:nat.∀h2:nat.(eq A (aplus g (aplus g a h1) h2) (aplus g a (plus h1 h2)))
BODY =
        assume g: G
        assume a: A
        assume h1: nat
          we proceed by induction on h1 to prove ∀h2:nat.(eq A (aplus g (aplus g a h1) h2) (aplus g a (plus h1 h2)))
             case O : ⇒
                the thesis becomes ∀h2:nat.(eq A (aplus g (aplus g a O) h2) (aplus g a (plus O h2)))
                   assume h2: nat
                      by (refl_equal . .)
                      we proved eq A (aplus g a h2) (aplus g a h2)
                      that is equivalent to eq A (aplus g (aplus g a O) h2) (aplus g a (plus O h2))
∀h2:nat.(eq A (aplus g (aplus g a O) h2) (aplus g a (plus O h2)))
             case S : n:nat ⇒
                the thesis becomes 
                ∀h2:nat
                  .eq
                    A
                    aplus g (asucc g (aplus g a n)) h2
                    asucc g (aplus g a (plus n h2))
                () by induction hypothesis we know ∀h2:nat.(eq A (aplus g (aplus g a n) h2) (aplus g a (plus n h2)))
                   assume h2: nat
                      we proceed by induction on h2 to prove 
                         eq
                           A
                           aplus g (asucc g (aplus g a n)) h2
                           asucc g (aplus g a (plus n h2))
                         case O : ⇒
                            the thesis becomes 
                            eq
                              A
                              aplus g (asucc g (aplus g a n)) O
                              asucc g (aplus g a (plus n O))
                               by (plus_n_O .)
                               we proved eq nat n (plus n O)
                               we proceed by induction on the previous result to prove eq A (asucc g (aplus g a n)) (asucc g (aplus g a (plus n O)))
                                  case refl_equal : ⇒
                                     the thesis becomes eq A (asucc g (aplus g a n)) (asucc g (aplus g a n))
                                        by (refl_equal . .)
eq A (asucc g (aplus g a n)) (asucc g (aplus g a n))
                               we proved eq A (asucc g (aplus g a n)) (asucc g (aplus g a (plus n O)))

                                  eq
                                    A
                                    aplus g (asucc g (aplus g a n)) O
                                    asucc g (aplus g a (plus n O))
                         case S : n0:nat ⇒
                            the thesis becomes 
                            eq
                              A
                              aplus g (asucc g (aplus g a n)) (S n0)
                              asucc g (aplus g a (plus n (S n0)))
                            (H0) by induction hypothesis we know 
                               eq
                                 A
                                 aplus g (asucc g (aplus g a n)) n0
                                 asucc g (aplus g a (plus n n0))
                               by (plus_n_Sm . .)
                               we proved eq nat (S (plus n n0)) (plus n (S n0))
                               we proceed by induction on the previous result to prove 
                                  eq
                                    A
                                    asucc g (aplus g (asucc g (aplus g a n)) n0)
                                    asucc g (aplus g a (plus n (S n0)))
                                  case refl_equal : ⇒
                                     the thesis becomes 
                                     eq
                                       A
                                       asucc g (aplus g (asucc g (aplus g a n)) n0)
                                       asucc g (aplus g a (S (plus n n0)))
                                        by (refl_equal . .)
                                        we proved eq G g g
                                        by (f_equal2 . . . . . . . . previous H0)
                                        we proved 
                                           eq
                                             A
                                             asucc g (aplus g (asucc g (aplus g a n)) n0)
                                             asucc g (asucc g (aplus g a (plus n n0)))

                                           eq
                                             A
                                             asucc g (aplus g (asucc g (aplus g a n)) n0)
                                             asucc g (aplus g a (S (plus n n0)))
                               we proved 
                                  eq
                                    A
                                    asucc g (aplus g (asucc g (aplus g a n)) n0)
                                    asucc g (aplus g a (plus n (S n0)))

                                  eq
                                    A
                                    aplus g (asucc g (aplus g a n)) (S n0)
                                    asucc g (aplus g a (plus n (S n0)))
                      we proved 
                         eq
                           A
                           aplus g (asucc g (aplus g a n)) h2
                           asucc g (aplus g a (plus n h2))
                      that is equivalent to eq A (aplus g (aplus g a (S n)) h2) (aplus g a (plus (S n) h2))

                      ∀h2:nat
                        .eq
                          A
                          aplus g (asucc g (aplus g a n)) h2
                          asucc g (aplus g a (plus n h2))
          we proved ∀h2:nat.(eq A (aplus g (aplus g a h1) h2) (aplus g a (plus h1 h2)))
       we proved ∀g:G.∀a:A.∀h1:nat.∀h2:nat.(eq A (aplus g (aplus g a h1) h2) (aplus g a (plus h1 h2)))