(plus n h2)))) H (\lambda (n: nat).(\lambda (H0: (eq A (aplus g a1 (plus n
h1)) (aplus g a2 (plus n h2)))).(f_equal2 G A A asucc g g (aplus g a1 (plus n
h1)) (aplus g a2 (plus n h2)) (refl_equal G g) H0))) h))))))).
(plus n h2)))) H (\lambda (n: nat).(\lambda (H0: (eq A (aplus g a1 (plus n
h1)) (aplus g a2 (plus n h2)))).(f_equal2 G A A asucc g g (aplus g a1 (plus n
h1)) (aplus g a2 (plus n h2)) (refl_equal G g) H0))) h))))))).