include "basic_1/drop/fwd.ma".
-theorem csuba_drop_abbr:
+lemma csuba_drop_abbr:
\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).((drop i
O c1 (CHead d1 (Bind Abbr) u)) \to (\forall (g: G).(\forall (c2: C).((csuba g
c1 c2) \to (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abbr) u)))
H8)) c2 H6))))) H5)))))) k H2 (drop_gen_drop k c (CHead d1 (Bind Abbr) u) t n
H1)))))))))))) c1)))) i).
-theorem csuba_drop_abst:
+lemma csuba_drop_abst:
\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop i
O c1 (CHead d1 (Bind Abst) u1)) \to (\forall (g: G).(\forall (c2: C).((csuba
g c1 c2) \to (or (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abst)
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).
-theorem csuba_drop_abst_rev:
+lemma csuba_drop_abst_rev:
\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).((drop i
O c1 (CHead d1 (Bind Abst) u)) \to (\forall (g: G).(\forall (c2: C).((csuba g
c2 c1) \to (or (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abst)
H8)) c2 H6))))) H5)))))) k H2 (drop_gen_drop k c (CHead d1 (Bind Abst) u) t n
H1)))))))))))) c1)))) i).
-theorem csuba_drop_abbr_rev:
+lemma csuba_drop_abbr_rev:
\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop i
O c1 (CHead d1 (Bind Abbr) u1)) \to (\forall (g: G).(\forall (c2: C).((csuba
g c2 c1) \to (or3 (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abbr)