(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/getl/props.ma".
+include "Basic-1/getl/props.ma".
-include "LambdaDelta-1/clear/drop.ma".
+include "Basic-1/clear/drop.ma".
theorem clear_getl_trans:
\forall (i: nat).(\forall (c2: C).(\forall (c3: C).((getl i c2 c3) \to
H6) H7)))) H5))))) (\lambda (f: F).(\lambda (_: (getl (S n) (CHead c (Flat f)
t) c3)).(\lambda (H4: (clear c1 (CHead c (Flat f) t))).(clear_gen_flat_r f c1
c t H4 (getl (S n) c1 c3))))) k H1 H2))))))))) c2)))) i).
+(* COMMENTS
+Initial nodes: 525
+END *)
theorem getl_clear_trans:
\forall (i: nat).(\forall (c1: C).(\forall (c2: C).((getl i c1 c2) \to
x0) x2) H5) in (eq_ind_r C (CHead x1 (Bind x0) x2) (\lambda (c: C).(getl i c1
c)) (getl_intro i c1 (CHead x1 (Bind x0) x2) x H2 H6) c3 (clear_gen_bind x0
x1 c3 x2 H7)))))))) H4))))) H1))))))).
+(* COMMENTS
+Initial nodes: 269
+END *)
theorem getl_clear_bind:
\forall (b: B).(\forall (c: C).(\forall (e1: C).(\forall (v: T).((clear c
(CHead c0 (Flat f) t) (CHead e1 (Bind b) v))).(getl_flat c0 e2 (S n) (H e1 v
(clear_gen_flat f c0 (CHead e1 (Bind b) v) t H2) e2 n H1) f t))) k
H0))))))))))) c)).
+(* COMMENTS
+Initial nodes: 599
+END *)
theorem getl_clear_conf:
\forall (i: nat).(\forall (c1: C).(\forall (c3: C).((getl i c1 c3) \to
(\lambda (f: F).(\lambda (H3: (getl (S n) (CHead c (Flat f) t) c3)).(\lambda
(H4: (clear (CHead c (Flat f) t) c2)).(H0 c3 (getl_gen_S (Flat f) c c3 t n
H3) c2 (clear_gen_flat f c c2 t H4))))) k H1 H2))))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 641
+END *)