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 =
Show proof