i c2 (CHead d2 (Bind Abbr) u))) (pr2 c2 t3 t) (\lambda (x: C).(\lambda (_:
(csubt g d x)).(\lambda (H6: (getl i c2 (CHead x (Bind Abbr) u))).(pr2_delta
c2 x u i H6 t3 t4 H1 t H2)))) H4)))))))))))))) c1 t1 t2 H))))).
i c2 (CHead d2 (Bind Abbr) u))) (pr2 c2 t3 t) (\lambda (x: C).(\lambda (_:
(csubt g d x)).(\lambda (H6: (getl i c2 (CHead x (Bind Abbr) u))).(pr2_delta
c2 x u i H6 t3 t4 H1 t H2)))) H4)))))))))))))) c1 t1 t2 H))))).