include "basic_1/getl/clear.ma".
-theorem csuba_getl_abbr:
+lemma csuba_getl_abbr:
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall
(i: nat).((getl i c1 (CHead d1 (Bind Abbr) u)) \to (\forall (c2: C).((csuba g
c1 c2) \to (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abbr) u)))
x9 (Bind Abbr) u) n H22) H23)))) H21)))))))) H17)))))) H14))))))) H11))))))))
i) H7))))) k H3 H4))))))) x H1 H2)))) H0))))))).
-theorem csuba_getl_abst:
+lemma csuba_getl_abst:
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).(\forall
(i: nat).((getl i c1 (CHead d1 (Bind Abst) u1)) \to (\forall (c2: C).((csuba
g c1 c2) \to (or (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst)
H21)))))))) H17)))))) H14))))))) H11)))))))) i) H7))))) k H3 H4))))))) x H1
H2)))) H0))))))).
-theorem csuba_getl_abst_rev:
+lemma csuba_getl_abst_rev:
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall
(i: nat).((getl i c1 (CHead d1 (Bind Abst) u)) \to (\forall (c2: C).((csuba g
c2 c1) \to (or (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u)))
Void) x10) n H23) H24)))))) H22)) H21)))))))) H17)))))) H14)))))))
H11)))))))) i) H7))))) k H3 H4))))))) x H1 H2)))) H0))))))).
-theorem csuba_getl_abbr_rev:
+lemma csuba_getl_abbr_rev:
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).(\forall
(i: nat).((getl i c1 (CHead d1 (Bind Abbr) u1)) \to (\forall (c2: C).((csuba
g c2 c1) \to (or3 (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abbr)