(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/getl/drop.ma".
+include "Basic-1/getl/drop.ma".
-include "LambdaDelta-1/getl/clear.ma".
+include "Basic-1/getl/clear.ma".
theorem getl_conf_le:
\forall (i: nat).(\forall (a: C).(\forall (c: C).((getl i c a) \to (\forall
a) (\lambda (x: C).(\lambda (H3: (drop h O c x)).(\lambda (H4: (clear x
e)).(getl_clear_conf (minus i h) x a (getl_drop_conf_ge i a c H x h O H3 H1)
e H4)))) H2))))))))).
+(* COMMENTS
+Initial nodes: 133
+END *)
theorem getl_trans:
\forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((getl
(getl (plus i0 h) c1 e2)))).(\lambda (H4: (drop (S i0) O c2 x)).(let H_y \def
(getl_drop_trans c1 c2 h H x i0 H4) in (getl_intro (plus (S i0) h) c1 e2 x
H_y H3))))) i H2)))) H1)))))))).
+(* COMMENTS
+Initial nodes: 247
+END *)