DEFINITION next_plus_assoc()
TYPE =
       ∀g:G
         .∀n:nat
           .∀h1:nat
             .∀h2:nat
               .eq
                 nat
                 next_plus g (next_plus g n h1) h2
                 next_plus g n (plus h1 h2)
BODY =
        assume g: G
        assume n: nat
        assume h1: nat
          we proceed by induction on h1 to prove 
             ∀h2:nat
               .eq
                 nat
                 next_plus g (next_plus g n h1) h2
                 next_plus g n (plus h1 h2)
             case O : ⇒
                the thesis becomes 
                ∀h2:nat
                  .eq
                    nat
                    next_plus g (next_plus g n O) h2
                    next_plus g n (plus O h2)
                   assume h2: nat
                      by (refl_equal . .)
                      we proved eq nat (next_plus g n h2) (next_plus g n h2)
                      that is equivalent to 
                         eq
                           nat
                           next_plus g (next_plus g n O) h2
                           next_plus g n (plus O h2)

                      ∀h2:nat
                        .eq
                          nat
                          next_plus g (next_plus g n O) h2
                          next_plus g n (plus O h2)
             case S : n0:nat ⇒
                the thesis becomes 
                ∀h2:nat
                  .eq
                    nat
                    next_plus g (next g (next_plus g n n0)) h2
                    next g (next_plus g n (plus n0 h2))
                () by induction hypothesis we know 
                   ∀h2:nat
                     .eq
                       nat
                       next_plus g (next_plus g n n0) h2
                       next_plus g n (plus n0 h2)
                   assume h2: nat
                      we proceed by induction on h2 to prove 
                         eq
                           nat
                           next_plus g (next g (next_plus g n n0)) h2
                           next g (next_plus g n (plus n0 h2))
                         case O : ⇒
                            the thesis becomes 
                            eq
                              nat
                              next_plus g (next g (next_plus g n n0)) O
                              next g (next_plus g n (plus n0 O))
                               by (plus_n_O .)
                               we proved eq nat n0 (plus n0 O)
                               we proceed by induction on the previous result to prove 
                                  eq
                                    nat
                                    next g (next_plus g n n0)
                                    next g (next_plus g n (plus n0 O))
                                  case refl_equal : ⇒
                                     the thesis becomes eq nat (next g (next_plus g n n0)) (next g (next_plus g n n0))
                                        by (refl_equal . .)
eq nat (next g (next_plus g n n0)) (next g (next_plus g n n0))
                               we proved 
                                  eq
                                    nat
                                    next g (next_plus g n n0)
                                    next g (next_plus g n (plus n0 O))

                                  eq
                                    nat
                                    next_plus g (next g (next_plus g n n0)) O
                                    next g (next_plus g n (plus n0 O))
                         case S : n1:nat ⇒
                            the thesis becomes 
                            eq
                              nat
                              next_plus g (next g (next_plus g n n0)) (S n1)
                              next g (next_plus g n (plus n0 (S n1)))
                            (H0) by induction hypothesis we know 
                               eq
                                 nat
                                 next_plus g (next g (next_plus g n n0)) n1
                                 next g (next_plus g n (plus n0 n1))
                               by (plus_n_Sm . .)
                               we proved eq nat (S (plus n0 n1)) (plus n0 (S n1))
                               we proceed by induction on the previous result to prove 
                                  eq
                                    nat
                                    next g (next_plus g (next g (next_plus g n n0)) n1)
                                    next g (next_plus g n (plus n0 (S n1)))
                                  case refl_equal : ⇒
                                     the thesis becomes 
                                     eq
                                       nat
                                       next g (next_plus g (next g (next_plus g n n0)) n1)
                                       next g (next_plus g n (S (plus n0 n1)))
                                        by (f_equal . . . . . H0)
                                        we proved 
                                           eq
                                             nat
                                             next g (next_plus g (next g (next_plus g n n0)) n1)
                                             next g (next g (next_plus g n (plus n0 n1)))

                                           eq
                                             nat
                                             next g (next_plus g (next g (next_plus g n n0)) n1)
                                             next g (next_plus g n (S (plus n0 n1)))
                               we proved 
                                  eq
                                    nat
                                    next g (next_plus g (next g (next_plus g n n0)) n1)
                                    next g (next_plus g n (plus n0 (S n1)))

                                  eq
                                    nat
                                    next_plus g (next g (next_plus g n n0)) (S n1)
                                    next g (next_plus g n (plus n0 (S n1)))
                      we proved 
                         eq
                           nat
                           next_plus g (next g (next_plus g n n0)) h2
                           next g (next_plus g n (plus n0 h2))
                      that is equivalent to 
                         eq
                           nat
                           next_plus g (next_plus g n (S n0)) h2
                           next_plus g n (plus (S n0) h2)

                      ∀h2:nat
                        .eq
                          nat
                          next_plus g (next g (next_plus g n n0)) h2
                          next g (next_plus g n (plus n0 h2))
          we proved 
             ∀h2:nat
               .eq
                 nat
                 next_plus g (next_plus g n h1) h2
                 next_plus g n (plus h1 h2)
       we proved 
          ∀g:G
            .∀n:nat
              .∀h1:nat
                .∀h2:nat
                  .eq
                    nat
                    next_plus g (next_plus g n h1) h2
                    next_plus g n (plus h1 h2)