DEFINITION next_plus_next()
TYPE =
       ∀g:G
         .∀n:nat
           .∀h:nat
             .eq nat (next_plus g (next g n) h) (next g (next_plus g n h))
BODY =
        assume g: G
        assume n: nat
        assume h: nat
          (h1) 
             by (refl_equal . .)
             we proved eq nat (next g (next_plus g n h)) (next g (next_plus g n h))

                eq
                  nat
                  next_plus g n (plus (S O) h)
                  next g (next_plus g n h)
          end of h1
          (h2) 
             by (next_plus_assoc . . . .)

                eq
                  nat
                  next_plus g (next_plus g n (S O)) h
                  next_plus g n (plus (S O) h)
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved 
             eq
               nat
               next_plus g (next_plus g n (S O)) h
               next g (next_plus g n h)
          that is equivalent to eq nat (next_plus g (next g n) h) (next g (next_plus g n h))
       we proved 
          ∀g:G
            .∀n:nat
              .∀h:nat
                .eq nat (next_plus g (next g n) h) (next g (next_plus g n h))