DEFINITION aplus_asucc()
TYPE =
       ∀g:G.∀h:nat.∀a:A.(eq A (aplus g (asucc g a) h) (asucc g (aplus g a h)))
BODY =
        assume g: G
        assume h: nat
        assume a: A
          (h1) 
             by (refl_equal . .)
             we proved eq A (asucc g (aplus g a h)) (asucc g (aplus g a h))
eq A (aplus g a (plus (S O) h)) (asucc g (aplus g a h))
          end of h1
          (h2) 
             by (aplus_assoc . . . .)
eq A (aplus g (aplus g a (S O)) h) (aplus g a (plus (S O) h))
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved eq A (aplus g (aplus g a (S O)) h) (asucc g (aplus g a h))
          that is equivalent to eq A (aplus g (asucc g a) h) (asucc g (aplus g a h))
       we proved ∀g:G.∀h:nat.∀a:A.(eq A (aplus g (asucc g a) h) (asucc g (aplus g a h)))