\forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr2 c1
t1 t2) \to (\forall (c2: C).((csubt g c1 c2) \to (pr2 c2 t1 t2)))))))
\def
\forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr2 c1
t1 t2) \to (\forall (c2: C).((csubt g c1 c2) \to (pr2 c2 t1 t2)))))))
\def
(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))))).
(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))))).
\forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pc3 c1
t1 t2) \to (\forall (c2: C).((csubt g c1 c2) \to (pc3 c2 t1 t2)))))))
\def
\forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pc3 c1
t1 t2) \to (\forall (c2: C).((csubt g c1 c2) \to (pc3 c2 t1 t2)))))))
\def