-(aplus g a n1)))) (sym_eq A (asucc g (asucc g (aplus g a (plus n n0))))
-(asucc g (aplus g (asucc g (aplus g a n)) n0)) (sym_eq A (asucc g (aplus g
-(asucc g (aplus g a n)) n0)) (asucc g (asucc g (aplus g a (plus n n0))))
-(sym_eq A (asucc g (asucc g (aplus g a (plus n n0)))) (asucc g (aplus g
-(asucc g (aplus g a n)) n0)) (f_equal2 G A A asucc g g (asucc g (aplus g a
-(plus n n0))) (aplus g (asucc g (aplus g a n)) n0) (refl_equal G g) (sym_eq A
-(aplus g (asucc g (aplus g a n)) n0) (asucc g (aplus g a (plus n n0)))
-H0))))) (plus n (S n0)) (plus_n_Sm n n0)))) h2)))) h1))).
+(aplus g a n1)))) (f_equal2 G A A asucc g g (aplus g (asucc g (aplus g a n))
+n0) (asucc g (aplus g a (plus n n0))) (refl_equal G g) H0) (plus n (S n0))
+(plus_n_Sm n n0)))) h2)))) h1))).