(\lambda (e2: C).(clear (CHead c4 (Bind Abbr) u) e2)) (CHead c4 (Bind Abbr)
u) (csuba_abst g c3 c4 H0 t a H2 u H3) (clear_bind Abbr c4 u)) e1
(clear_gen_bind Abst c3 e1 t H4))))))))))))) c1 c2 H)))).
(\lambda (e2: C).(clear (CHead c4 (Bind Abbr) u) e2)) (CHead c4 (Bind Abbr)
u) (csuba_abst g c3 c4 H0 t a H2 u H3) (clear_bind Abbr c4 u)) e1
(clear_gen_bind Abst c3 e1 t H4))))))))))))) c1 c2 H)))).