(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csuba/fwd.ma".
+include "Basic-1/csuba/fwd.ma".
-include "LambdaDelta-1/drop/fwd.ma".
+include "Basic-1/drop/fwd.ma".
theorem csuba_drop_abbr:
\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).((drop i
d1 d2)) x (drop_drop (Flat f) n x0 (CHead x (Bind Abbr) u) H9 x1) H10))))
H8)) c2 H6))))) H5)))))) k H2 (drop_gen_drop k c (CHead d1 (Bind Abbr) u) t n
H1)))))))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 3648
+END *)
theorem csuba_drop_abst:
\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop i
A).(arity g d2 u2 a)))) x2 x3 x4 (drop_drop (Flat f) n x0 (CHead x2 (Bind
Abbr) x3) H10 x1) H11 H12 H13))))))))) H9)) H8)) c2 H6))))) H5)))))) k H2
(drop_gen_drop k c (CHead d1 (Bind Abst) u1) t n H1)))))))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 12528
+END *)
theorem csuba_drop_abst_rev:
\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).((drop i
(drop_drop (Flat f) n x0 (CHead x2 (Bind Void) x3) H10 x1) H11)))))) H9))
H8)) c2 H6))))) H5)))))) k H2 (drop_gen_drop k c (CHead d1 (Bind Abst) u) t n
H1)))))))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 11438
+END *)
theorem csuba_drop_abbr_rev:
\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop i
(d2: C).(\lambda (_: T).(csuba g d2 d1))) x2 x3 (drop_drop (Flat f) n x0
(CHead x2 (Bind Void) x3) H10 x1) H11)))))) H9)) H8)) c2 H6))))) H5)))))) k
H2 (drop_gen_drop k c (CHead d1 (Bind Abbr) u1) t n H1)))))))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 23852
+END *)