T).(\lambda (_: nat).(arity g d u (asucc g b))))) x0 x1 x2 H8 (arity_repl g
x0 x1 (asucc g x) H9 (asucc g b) (asucc_repl g x b H5)))))))) H7))))))
H4))))))))))))) c t a H))))).
T).(\lambda (_: nat).(arity g d u (asucc g b))))) x0 x1 x2 H8 (arity_repl g
x0 x1 (asucc g x) H9 (asucc g b) (asucc_repl g x b H5)))))))) H7))))))
H4))))))))))))) c t a H))))).