DEFINITION aplus_reg_r()
TYPE =
       ∀g:G
         .∀a1:A
           .∀a2:A
             .∀h1:nat
               .∀h2:nat
                 .eq A (aplus g a1 h1) (aplus g a2 h2)
                   →∀h:nat.(eq A (aplus g a1 (plus h h1)) (aplus g a2 (plus h h2)))
BODY =
Show proof