(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/getl/fwd.ma".
+include "Basic-1/getl/fwd.ma".
-include "LambdaDelta-1/drop/props.ma".
+include "Basic-1/drop/props.ma".
-include "LambdaDelta-1/clear/props.ma".
+include "Basic-1/clear/props.ma".
theorem getl_refl:
\forall (b: B).(\forall (c: C).(\forall (u: T).(getl O (CHead c (Bind b) u)
\lambda (b: B).(\lambda (c: C).(\lambda (u: T).(getl_intro O (CHead c (Bind
b) u) (CHead c (Bind b) u) (CHead c (Bind b) u) (drop_refl (CHead c (Bind b)
u)) (clear_bind b c u)))).
+(* COMMENTS
+Initial nodes: 59
+END *)
theorem getl_head:
\forall (k: K).(\forall (h: nat).(\forall (c: C).(\forall (e: C).((getl (r k
C).(clear e0 e)) (getl (S h) (CHead c k u) e) (\lambda (x: C).(\lambda (H1:
(drop (r k h) O c x)).(\lambda (H2: (clear x e)).(getl_intro (S h) (CHead c k
u) e x (drop_drop k h c x H1 u) H2)))) H0))))))).
+(* COMMENTS
+Initial nodes: 137
+END *)
theorem getl_flat:
\forall (c: C).(\forall (e: C).(\forall (h: nat).((getl h c e) \to (\forall
(((drop h0 O c x) \to (getl h0 (CHead c (Flat f) u) e)))).(\lambda (H3: (drop
(S h0) O c x)).(getl_intro (S h0) (CHead c (Flat f) u) e x (drop_drop (Flat
f) h0 c x H3 u) H2)))) h H1)))) H0))))))).
+(* COMMENTS
+Initial nodes: 285
+END *)
theorem getl_ctail:
\forall (b: B).(\forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i:
C).(\lambda (H1: (drop i O c x)).(\lambda (H2: (clear x (CHead d (Bind b)
u))).(getl_intro i (CTail k v c) (CHead (CTail k v d) (Bind b) u) (CTail k v
x) (drop_ctail c x O i H1 k v) (clear_ctail b x d u H2 k v))))) H0))))))))).
+(* COMMENTS
+Initial nodes: 203
+END *)
theorem getl_mono:
\forall (c: C).(\forall (x1: C).(\forall (h: nat).((getl h c x1) \to
C).(drop h O c c0)) H7 x (drop_mono c x O h H2 x0 H5)) in (let H9 \def
(eq_ind_r C x0 (\lambda (c0: C).(clear c0 x1)) H6 x (drop_mono c x O h H2 x0
H5)) in (clear_mono x x1 H9 x2 H3))))))) H4))))) H1))))))).
+(* COMMENTS
+Initial nodes: 269
+END *)