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