d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Bind
Abst) t) (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba
g d2 d1))))) H6)))))))))))) c y H0))) H))))).
d1))) (ex2_2 C T (\lambda (d2: C).(\lambda (u2: T).(eq C (CHead c1 (Bind
Abst) t) (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba
g d2 d1))))) H6)))))))))))) c y H0))) H))))).