(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csubv/clear.ma".
+include "Basic-1/csubv/clear.ma".
-include "LambdaDelta-1/csubv/drop.ma".
+include "Basic-1/csubv/drop.ma".
-include "LambdaDelta-1/getl/fwd.ma".
+include "Basic-1/getl/fwd.ma".
theorem csubv_getl_conf:
\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (b1:
(\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(getl i c2 (CHead d2 (Bind
b2) v2))))) x1 x2 x3 H8 (getl_intro i c2 (CHead x2 (Bind x1) x3) x0 H6
H9))))))) H7)))))) H4)))))) H1))))))))).
+(* COMMENTS
+Initial nodes: 455
+END *)
theorem csubv_getl_conf_void:
\forall (c1: C).(\forall (c2: C).((csubv c1 c2) \to (\forall (d1:
(\lambda (d2: C).(\lambda (_: T).(csubv d1 d2))) (\lambda (d2: C).(\lambda
(v2: T).(getl i c2 (CHead d2 (Bind Void) v2)))) x1 x2 H8 (getl_intro i c2
(CHead x1 (Bind Void) x2) x0 H6 H9)))))) H7)))))) H4)))))) H1)))))))).
+(* COMMENTS
+Initial nodes: 417
+END *)