DEFINITION aplus_ahead_simpl()
TYPE =
       ∀g:G.∀h:nat.∀a1:A.∀a2:A.(eq A (aplus g (AHead a1 a2) h) (AHead a1 (aplus g a2 h)))
BODY =
        assume g: G
        assume h: nat
          we proceed by induction on h to prove ∀a1:A.∀a2:A.(eq A (aplus g (AHead a1 a2) h) (AHead a1 (aplus g a2 h)))
             case O : ⇒
                the thesis becomes ∀a1:A.∀a2:A.(eq A (aplus g (AHead a1 a2) O) (AHead a1 (aplus g a2 O)))
                    assume a1: A
                    assume a2: A
                      by (refl_equal . .)
                      we proved eq A (AHead a1 a2) (AHead a1 a2)
                      that is equivalent to eq A (aplus g (AHead a1 a2) O) (AHead a1 (aplus g a2 O))
∀a1:A.∀a2:A.(eq A (aplus g (AHead a1 a2) O) (AHead a1 (aplus g a2 O)))
             case S : n:nat ⇒
                the thesis becomes 
                ∀a1:A
                  .∀a2:A
                    .eq
                      A
                      asucc g (aplus g (AHead a1 a2) n)
                      AHead a1 (asucc g (aplus g a2 n))
                (H) by induction hypothesis we know ∀a1:A.∀a2:A.(eq A (aplus g (AHead a1 a2) n) (AHead a1 (aplus g a2 n)))
                    assume a1: A
                    assume a2: A
                      by (aplus_asucc . . .)
                      we proved 
                         eq
                           A
                           aplus g (asucc g (AHead a1 a2)) n
                           asucc g (aplus g (AHead a1 a2) n)
                      we proceed by induction on the previous result to prove 
                         eq
                           A
                           asucc g (aplus g (AHead a1 a2) n)
                           AHead a1 (asucc g (aplus g a2 n))
                         case refl_equal : ⇒
                            the thesis becomes 
                            eq
                              A
                              aplus g (asucc g (AHead a1 a2)) n
                              AHead a1 (asucc g (aplus g a2 n))
                               by (aplus_asucc . . .)
                               we proved eq A (aplus g (asucc g a2) n) (asucc g (aplus g a2 n))
                               we proceed by induction on the previous result to prove 
                                  eq
                                    A
                                    aplus g (asucc g (AHead a1 a2)) n
                                    AHead a1 (asucc g (aplus g a2 n))
                                  case refl_equal : ⇒
                                     the thesis becomes 
                                     eq
                                       A
                                       aplus g (asucc g (AHead a1 a2)) n
                                       AHead a1 (aplus g (asucc g a2) n)
                                        by (H . .)
                                        we proved 
                                           eq
                                             A
                                             aplus g (AHead a1 (asucc g a2)) n
                                             AHead a1 (aplus g (asucc g a2) n)

                                           eq
                                             A
                                             aplus g (asucc g (AHead a1 a2)) n
                                             AHead a1 (aplus g (asucc g a2) n)

                                  eq
                                    A
                                    aplus g (asucc g (AHead a1 a2)) n
                                    AHead a1 (asucc g (aplus g a2 n))
                      we proved 
                         eq
                           A
                           asucc g (aplus g (AHead a1 a2) n)
                           AHead a1 (asucc g (aplus g a2 n))
                      that is equivalent to eq A (aplus g (AHead a1 a2) (S n)) (AHead a1 (aplus g a2 (S n)))

                      ∀a1:A
                        .∀a2:A
                          .eq
                            A
                            asucc g (aplus g (AHead a1 a2) n)
                            AHead a1 (asucc g (aplus g a2 n))
          we proved ∀a1:A.∀a2:A.(eq A (aplus g (AHead a1 a2) h) (AHead a1 (aplus g a2 h)))
       we proved ∀g:G.∀h:nat.∀a1:A.∀a2:A.(eq A (aplus g (AHead a1 a2) h) (AHead a1 (aplus g a2 h)))