(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csubt/getl.ma".
+include "Basic-1/csubt/getl.ma".
-include "LambdaDelta-1/pc3/left.ma".
+include "Basic-1/pc3/left.ma".
theorem csubt_pr2:
\forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr2 c1
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))))).
+(* COMMENTS
+Initial nodes: 245
+END *)
theorem csubt_pc3:
\forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pc3 c1
(c2: C).((csubt g c1 c2) \to (pc3 c2 t0 t4))))).(\lambda (c2: C).(\lambda
(H3: (csubt g c1 c2)).(pc3_t t0 c2 t3 (pc3_pr2_x c2 t3 t0 (csubt_pr2 g c1 t0
t3 H0 c2 H3)) t4 (H2 c2 H3)))))))))) t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 245
+END *)