(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csubt/fwd.ma".
+include "Basic-1/csubt/fwd.ma".
-include "LambdaDelta-1/drop/fwd.ma".
+include "Basic-1/drop/fwd.ma".
theorem csubt_drop_flat:
\forall (g: G).(\forall (f: F).(\forall (n: nat).(\forall (c1: C).(\forall
u0))) x H6 (drop_drop (Bind Abbr) n0 c3 (CHead x (Flat f) u0) H7 u))))) (H c0
c3 H1 d1 u0 (drop_gen_drop (Bind Abst) c0 (CHead d1 (Flat f) u0) t n0
H5)))))))))))))) c1 c2 H0)))))) n))).
+(* COMMENTS
+Initial nodes: 2090
+END *)
theorem csubt_drop_abbr:
\forall (g: G).(\forall (n: nat).(\forall (c1: C).(\forall (c2: C).((csubt g
(CHead d2 (Bind Abbr) u0))) x H6 (drop_drop (Bind Abbr) n0 c3 (CHead x (Bind
Abbr) u0) H7 u))))) (H c0 c3 H1 d1 u0 (drop_gen_drop (Bind Abst) c0 (CHead d1
(Bind Abbr) u0) t n0 H5)))))))))))))) c1 c2 H0)))))) n)).
+(* COMMENTS
+Initial nodes: 2084
+END *)
theorem csubt_drop_abst:
\forall (g: G).(\forall (n: nat).(\forall (c1: C).(\forall (c2: C).((csubt g
g d2 u0 t0))) x0 x1 H7 (drop_drop (Bind Abbr) n0 c3 (CHead x0 (Bind Abbr) x1)
H8 u) H9 H10)))))))) H6)) (H c0 c3 H1 d1 t0 (drop_gen_drop (Bind Abst) c0
(CHead d1 (Bind Abst) t0) t n0 H5)))))))))))))) c1 c2 H0)))))) n)).
+(* COMMENTS
+Initial nodes: 7940
+END *)