(* This file was automatically generated: do not edit *********************)
-include "getl/defs.ma".
+include "LambdaDelta-1/getl/defs.ma".
-include "drop/fwd.ma".
+include "LambdaDelta-1/drop/fwd.ma".
-include "clear/fwd.ma".
+include "LambdaDelta-1/clear/fwd.ma".
theorem getl_gen_all:
\forall (c1: C).(\forall (c2: C).(\forall (i: nat).((getl i c1 c2) \to (ex2
C (\lambda (e: C).(drop i O c1 e)) (\lambda (e: C).(clear e c2))))))
\def
\lambda (c1: C).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H: (getl i c1
-c2)).(let H0 \def (match H in getl return (\lambda (_: (getl ? ? ?)).(ex2 C
-(\lambda (e: C).(drop i O c1 e)) (\lambda (e: C).(clear e c2)))) with
-[(getl_intro e H0 H1) \Rightarrow (ex_intro2 C (\lambda (e0: C).(drop i O c1
-e0)) (\lambda (e0: C).(clear e0 c2)) e H0 H1)]) in H0)))).
+c2)).(getl_ind i c1 c2 (ex2 C (\lambda (e: C).(drop i O c1 e)) (\lambda (e:
+C).(clear e c2))) (\lambda (e: C).(\lambda (H0: (drop i O c1 e)).(\lambda
+(H1: (clear e c2)).(ex_intro2 C (\lambda (e0: C).(drop i O c1 e0)) (\lambda
+(e0: C).(clear e0 c2)) e H0 H1)))) H)))).
theorem getl_gen_sort:
\forall (n: nat).(\forall (h: nat).(\forall (x: C).((getl h (CSort n) x) \to
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))))))