(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csubt/clear.ma".
+include "Basic-1/csubt/clear.ma".
-include "LambdaDelta-1/csubt/drop.ma".
+include "Basic-1/csubt/drop.ma".
-include "LambdaDelta-1/getl/clear.ma".
+include "Basic-1/getl/clear.ma".
theorem csubt_getl_abbr:
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall
(getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Abbr) u) n0 H23)))))
H21)))))))) H17))))) H14))))))) H11)))))))) n) H7))))) k H3 H4))))))) x H1
H2)))) H0))))))).
+(* COMMENTS
+Initial nodes: 2313
+END *)
theorem csubt_getl_abst:
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (t: T).(\forall
g d2 u t))) x9 x10 H23 (getl_clear_bind x6 c2 x7 x8 H20 (CHead x9 (Bind Abbr)
x10) n0 H24) H25 H26)))))))) H22)) H21)))))))) H17))))) H14)))))))
H11)))))))) n) H7))))) k H3 H4))))))) x H1 H2)))) H0))))))).
+(* COMMENTS
+Initial nodes: 5861
+END *)