(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csubt/pc3.ma".
+include "Basic-1/csubt/pc3.ma".
-include "LambdaDelta-1/csubt/props.ma".
+include "Basic-1/csubt/props.ma".
theorem csubt_ty3:
\forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c1
T).(\lambda (_: (ty3 g c t3 t4)).(\lambda (H3: ((\forall (c2: C).((csubt g c
c2) \to (ty3 g c2 t3 t4))))).(\lambda (c2: C).(\lambda (H4: (csubt g c
c2)).(ty3_cast g c2 t0 t3 (H1 c2 H4) t4 (H3 c2 H4)))))))))))) c1 t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 1325
+END *)
theorem csubt_ty3_ld:
\forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (v: T).((ty3 g c u
(ty3 g c u v)).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (ty3 g (CHead
c (Bind Abst) v) t1 t2)).(csubt_ty3 g (CHead c (Bind Abst) v) t1 t2 H0 (CHead
c (Bind Abbr) u) (csubt_abst g c c (csubt_refl g c) u v H H))))))))).
+(* COMMENTS
+Initial nodes: 91
+END *)