(* This file was automatically generated: do not edit *********************)
-include "Basic-1/getl/drop.ma".
+include "basic_1/getl/drop.ma".
-include "Basic-1/getl/clear.ma".
+include "basic_1/getl/clear.ma".
-theorem getl_conf_le:
+lemma getl_conf_le:
\forall (i: nat).(\forall (a: C).(\forall (c: C).((getl i c a) \to (\forall
(e: C).(\forall (h: nat).((getl h c e) \to ((le h i) \to (getl (minus i h) e
a))))))))
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 *)