(CHead d (Bind Abst) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u
(asucc g a2)))) x0 x1 H10 (arity_repl g x0 x1 (asucc g a1) H11 (asucc g a2)
(asucc_repl g a1 a2 H3)))))))) H9)) H8))))))))))))) c y a H0))) H))))).
(CHead d (Bind Abst) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u
(asucc g a2)))) x0 x1 H10 (arity_repl g x0 x1 (asucc g a1) H11 (asucc g a2)
(asucc_repl g a1 a2 H3)))))))) H9)) H8))))))))))))) c y a H0))) H))))).