(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csuba/drop.ma".
+include "Basic-1/csuba/drop.ma".
-include "LambdaDelta-1/csuba/clear.ma".
+include "Basic-1/csuba/clear.ma".
-include "LambdaDelta-1/getl/clear.ma".
+include "Basic-1/getl/clear.ma".
theorem csuba_getl_abbr:
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall
(\lambda (d2: C).(csuba g d1 d2)) x9 (getl_clear_bind x6 c2 x7 x8 H20 (CHead
x9 (Bind Abbr) u) n H22) H23)))) H21)))))))) H17)))))) H14))))))) H11))))))))
i) H7))))) k H3 H4))))))) x H1 H2)))) H0))))))).
+(* COMMENTS
+Initial nodes: 2319
+END *)
theorem csuba_getl_abst:
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).(\forall
c2 x7 x8 H20 (CHead x9 (Bind Abbr) x10) n H23) H24 H25 H26))))))))) H22))
H21)))))))) H17)))))) H14))))))) H11)))))))) i) H7))))) k H3 H4))))))) x H1
H2)))) H0))))))).
+(* COMMENTS
+Initial nodes: 6437
+END *)
theorem csuba_getl_abst_rev:
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall
(getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Void) x10) n H23) H24))))))
H22)) H21)))))))) H17)))))) H14))))))) H11)))))))) i) H7))))) k H3 H4)))))))
x H1 H2)))) H0))))))).
+(* COMMENTS
+Initial nodes: 4703
+END *)
theorem csuba_getl_abbr_rev:
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).(\forall
(getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Void) x10) n H23) H24))))))
H22)) H21)))))))) H17)))))) H14))))))) H11)))))))) i) H7))))) k H3 H4)))))))
x H1 H2)))) H0))))))).
+(* COMMENTS
+Initial nodes: 9091
+END *)