C).(\lambda (H1: (drop (S h) O (CHead c k u) x0)).(\lambda (H2: (clear x0
x)).(getl_intro (r k h) c x x0 (drop_gen_drop k c x0 u h H1) H2)))) H0))))))).
+theorem getl_gen_2:
+ \forall (c1: C).(\forall (c2: C).(\forall (i: nat).((getl i c1 c2) \to (ex_3
+B C T (\lambda (b: B).(\lambda (c: C).(\lambda (v: T).(eq C c2 (CHead c (Bind
+b) v)))))))))
+\def
+ \lambda (c1: C).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H: (getl i c1
+c2)).(let H0 \def (getl_gen_all c1 c2 i H) in (ex2_ind C (\lambda (e:
+C).(drop i O c1 e)) (\lambda (e: C).(clear e c2)) (ex_3 B C T (\lambda (b:
+B).(\lambda (c: C).(\lambda (v: T).(eq C c2 (CHead c (Bind b) v))))))
+(\lambda (x: C).(\lambda (_: (drop i O c1 x)).(\lambda (H2: (clear x
+c2)).(let H3 \def (clear_gen_all x c2 H2) in (ex_3_ind B C T (\lambda (b:
+B).(\lambda (e: C).(\lambda (u: T).(eq C c2 (CHead e (Bind b) u))))) (ex_3 B
+C T (\lambda (b: B).(\lambda (c: C).(\lambda (v: T).(eq C c2 (CHead c (Bind
+b) v)))))) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H4:
+(eq C c2 (CHead x1 (Bind x0) x2))).(let H5 \def (eq_ind C c2 (\lambda (c:
+C).(clear x c)) H2 (CHead x1 (Bind x0) x2) H4) in (eq_ind_r C (CHead x1 (Bind
+x0) x2) (\lambda (c: C).(ex_3 B C T (\lambda (b: B).(\lambda (c0: C).(\lambda
+(v: T).(eq C c (CHead c0 (Bind b) v))))))) (ex_3_intro B C T (\lambda (b:
+B).(\lambda (c: C).(\lambda (v: T).(eq C (CHead x1 (Bind x0) x2) (CHead c
+(Bind b) v))))) x0 x1 x2 (refl_equal C (CHead x1 (Bind x0) x2))) c2 H4))))))
+H3))))) H0))))).
+
theorem getl_gen_flat:
\forall (f: F).(\forall (e: C).(\forall (d: C).(\forall (v: T).(\forall (i:
nat).((getl i (CHead e (Flat f) v) d) \to (getl i e d))))))