(* This file was automatically generated: do not edit *********************)
-include "csubc/defs.ma".
+include "LambdaDelta-1/csubc/fwd.ma".
-include "sc3/props.ma".
+include "LambdaDelta-1/sc3/props.ma".
theorem csubc_drop_conf_O:
\forall (g: G).(\forall (c1: C).(\forall (e1: C).(\forall (h: nat).((drop h
(((drop n O (CHead c k t) e1) \to (\forall (c2: C).((csubc g (CHead c k t)
c2) \to (ex2 C (\lambda (e2: C).(drop n O c2 e2)) (\lambda (e2: C).(csubc g
e1 e2)))))))).(\lambda (H1: (drop (S n) O (CHead c k t) e1)).(\lambda (c2:
-C).(\lambda (H2: (csubc g (CHead c k t) c2)).(let H3 \def (match H2 in csubc
-return (\lambda (c0: C).(\lambda (c3: C).(\lambda (_: (csubc ? c0 c3)).((eq C
-c0 (CHead c k t)) \to ((eq C c3 c2) \to (ex2 C (\lambda (e2: C).(drop (S n) O
-c2 e2)) (\lambda (e2: C).(csubc g e1 e2)))))))) with [(csubc_sort n0)
-\Rightarrow (\lambda (H3: (eq C (CSort n0) (CHead c k t))).(\lambda (H4: (eq
-C (CSort n0) c2)).((let H5 \def (eq_ind C (CSort n0) (\lambda (e: C).(match e
-in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _
-_ _) \Rightarrow False])) I (CHead c k t) H3) in (False_ind ((eq C (CSort n0)
-c2) \to (ex2 C (\lambda (e2: C).(drop (S n) O c2 e2)) (\lambda (e2: C).(csubc
-g e1 e2)))) H5)) H4))) | (csubc_head c0 c3 H3 k0 v) \Rightarrow (\lambda (H4:
-(eq C (CHead c0 k0 v) (CHead c k t))).(\lambda (H5: (eq C (CHead c3 k0 v)
-c2)).((let H6 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda
-(_: C).T) with [(CSort _) \Rightarrow v | (CHead _ _ t0) \Rightarrow t0]))
-(CHead c0 k0 v) (CHead c k t) H4) in ((let H7 \def (f_equal C K (\lambda (e:
-C).(match e in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k0 |
-(CHead _ k1 _) \Rightarrow k1])) (CHead c0 k0 v) (CHead c k t) H4) in ((let
-H8 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C)
-with [(CSort _) \Rightarrow c0 | (CHead c4 _ _) \Rightarrow c4])) (CHead c0
-k0 v) (CHead c k t) H4) in (eq_ind C c (\lambda (c4: C).((eq K k0 k) \to ((eq
-T v t) \to ((eq C (CHead c3 k0 v) c2) \to ((csubc g c4 c3) \to (ex2 C
-(\lambda (e2: C).(drop (S n) O c2 e2)) (\lambda (e2: C).(csubc g e1
-e2)))))))) (\lambda (H9: (eq K k0 k)).(eq_ind K k (\lambda (k1: K).((eq T v
-t) \to ((eq C (CHead c3 k1 v) c2) \to ((csubc g c c3) \to (ex2 C (\lambda
-(e2: C).(drop (S n) O c2 e2)) (\lambda (e2: C).(csubc g e1 e2))))))) (\lambda
-(H10: (eq T v t)).(eq_ind T t (\lambda (t0: T).((eq C (CHead c3 k t0) c2) \to
-((csubc g c c3) \to (ex2 C (\lambda (e2: C).(drop (S n) O c2 e2)) (\lambda
-(e2: C).(csubc g e1 e2)))))) (\lambda (H11: (eq C (CHead c3 k t) c2)).(eq_ind
-C (CHead c3 k t) (\lambda (c4: C).((csubc g c c3) \to (ex2 C (\lambda (e2:
-C).(drop (S n) O c4 e2)) (\lambda (e2: C).(csubc g e1 e2))))) (\lambda (H12:
-(csubc g c c3)).(let H_x \def (H e1 (r k n) (drop_gen_drop k c e1 t n H1) c3
-H12) in (let H13 \def H_x in (ex2_ind C (\lambda (e2: C).(drop (r k n) O c3
-e2)) (\lambda (e2: C).(csubc g e1 e2)) (ex2 C (\lambda (e2: C).(drop (S n) O
-(CHead c3 k t) e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda (x:
-C).(\lambda (H14: (drop (r k n) O c3 x)).(\lambda (H15: (csubc g e1
-x)).(ex_intro2 C (\lambda (e2: C).(drop (S n) O (CHead c3 k t) e2)) (\lambda
-(e2: C).(csubc g e1 e2)) x (drop_drop k n c3 x H14 t) H15)))) H13)))) c2
-H11)) v (sym_eq T v t H10))) k0 (sym_eq K k0 k H9))) c0 (sym_eq C c0 c H8)))
-H7)) H6)) H5 H3))) | (csubc_abst c0 c3 H3 v a H4 w H5) \Rightarrow (\lambda
-(H6: (eq C (CHead c0 (Bind Abst) v) (CHead c k t))).(\lambda (H7: (eq C
-(CHead c3 (Bind Abbr) w) c2)).((let H8 \def (f_equal C T (\lambda (e:
-C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow v |
-(CHead _ _ t0) \Rightarrow t0])) (CHead c0 (Bind Abst) v) (CHead c k t) H6)
-in ((let H9 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda
-(_: C).K) with [(CSort _) \Rightarrow (Bind Abst) | (CHead _ k0 _)
-\Rightarrow k0])) (CHead c0 (Bind Abst) v) (CHead c k t) H6) in ((let H10
-\def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C)
-with [(CSort _) \Rightarrow c0 | (CHead c4 _ _) \Rightarrow c4])) (CHead c0
-(Bind Abst) v) (CHead c k t) H6) in (eq_ind C c (\lambda (c4: C).((eq K (Bind
-Abst) k) \to ((eq T v t) \to ((eq C (CHead c3 (Bind Abbr) w) c2) \to ((csubc
-g c4 c3) \to ((sc3 g (asucc g a) c4 v) \to ((sc3 g a c3 w) \to (ex2 C
-(\lambda (e2: C).(drop (S n) O c2 e2)) (\lambda (e2: C).(csubc g e1
-e2)))))))))) (\lambda (H11: (eq K (Bind Abst) k)).(eq_ind K (Bind Abst)
-(\lambda (_: K).((eq T v t) \to ((eq C (CHead c3 (Bind Abbr) w) c2) \to
-((csubc g c c3) \to ((sc3 g (asucc g a) c v) \to ((sc3 g a c3 w) \to (ex2 C
-(\lambda (e2: C).(drop (S n) O c2 e2)) (\lambda (e2: C).(csubc g e1
-e2))))))))) (\lambda (H12: (eq T v t)).(eq_ind T t (\lambda (t0: T).((eq C
-(CHead c3 (Bind Abbr) w) c2) \to ((csubc g c c3) \to ((sc3 g (asucc g a) c
-t0) \to ((sc3 g a c3 w) \to (ex2 C (\lambda (e2: C).(drop (S n) O c2 e2))
-(\lambda (e2: C).(csubc g e1 e2)))))))) (\lambda (H13: (eq C (CHead c3 (Bind
-Abbr) w) c2)).(eq_ind C (CHead c3 (Bind Abbr) w) (\lambda (c4: C).((csubc g c
-c3) \to ((sc3 g (asucc g a) c t) \to ((sc3 g a c3 w) \to (ex2 C (\lambda (e2:
-C).(drop (S n) O c4 e2)) (\lambda (e2: C).(csubc g e1 e2))))))) (\lambda
-(H14: (csubc g c c3)).(\lambda (_: (sc3 g (asucc g a) c t)).(\lambda (_: (sc3
-g a c3 w)).(let H17 \def (eq_ind_r K k (\lambda (k0: K).(drop (r k0 n) O c
-e1)) (drop_gen_drop k c e1 t n H1) (Bind Abst) H11) in (let H18 \def
-(eq_ind_r K k (\lambda (k0: K).((drop n O (CHead c k0 t) e1) \to (\forall
-(c4: C).((csubc g (CHead c k0 t) c4) \to (ex2 C (\lambda (e2: C).(drop n O c4
-e2)) (\lambda (e2: C).(csubc g e1 e2))))))) H0 (Bind Abst) H11) in (let H_x
-\def (H e1 (r (Bind Abst) n) H17 c3 H14) in (let H19 \def H_x in (ex2_ind C
-(\lambda (e2: C).(drop (r (Bind Abst) n) O c3 e2)) (\lambda (e2: C).(csubc g
-e1 e2)) (ex2 C (\lambda (e2: C).(drop (S n) O (CHead c3 (Bind Abbr) w) e2))
-(\lambda (e2: C).(csubc g e1 e2))) (\lambda (x: C).(\lambda (H20: (drop (r
-(Bind Abst) n) O c3 x)).(\lambda (H21: (csubc g e1 x)).(ex_intro2 C (\lambda
-(e2: C).(drop (S n) O (CHead c3 (Bind Abbr) w) e2)) (\lambda (e2: C).(csubc g
-e1 e2)) x (drop_drop (Bind Abbr) n c3 x H20 w) H21)))) H19)))))))) c2 H13)) v
-(sym_eq T v t H12))) k H11)) c0 (sym_eq C c0 c H10))) H9)) H8)) H7 H3 H4
-H5)))]) in (H3 (refl_equal C (CHead c k t)) (refl_equal C c2)))))))) h)))))))
-c1)).
+C).(\lambda (H2: (csubc g (CHead c k t) c2)).(let H_x \def (csubc_gen_head_l
+g c c2 t k H2) in (let H3 \def H_x in (or_ind (ex2 C (\lambda (c3: C).(eq C
+c2 (CHead c3 k t))) (\lambda (c3: C).(csubc g c c3))) (ex5_3 C T A (\lambda
+(_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst))))) (\lambda (c3:
+C).(\lambda (w: T).(\lambda (_: A).(eq C c2 (CHead c3 (Bind Abbr) w)))))
+(\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g c c3)))) (\lambda
+(_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) c t)))) (\lambda
+(c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w))))) (ex2 C (\lambda
+(e2: C).(drop (S n) O c2 e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda
+(H4: (ex2 C (\lambda (c3: C).(eq C c2 (CHead c3 k t))) (\lambda (c3:
+C).(csubc g c c3)))).(ex2_ind C (\lambda (c3: C).(eq C c2 (CHead c3 k t)))
+(\lambda (c3: C).(csubc g c c3)) (ex2 C (\lambda (e2: C).(drop (S n) O c2
+e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda (x: C).(\lambda (H5: (eq C
+c2 (CHead x k t))).(\lambda (H6: (csubc g c x)).(eq_ind_r C (CHead x k t)
+(\lambda (c0: C).(ex2 C (\lambda (e2: C).(drop (S n) O c0 e2)) (\lambda (e2:
+C).(csubc g e1 e2)))) (let H_x0 \def (H e1 (r k n) (drop_gen_drop k c e1 t n
+H1) x H6) in (let H7 \def H_x0 in (ex2_ind C (\lambda (e2: C).(drop (r k n) O
+x e2)) (\lambda (e2: C).(csubc g e1 e2)) (ex2 C (\lambda (e2: C).(drop (S n)
+O (CHead x k t) e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda (x0:
+C).(\lambda (H8: (drop (r k n) O x x0)).(\lambda (H9: (csubc g e1
+x0)).(ex_intro2 C (\lambda (e2: C).(drop (S n) O (CHead x k t) e2)) (\lambda
+(e2: C).(csubc g e1 e2)) x0 (drop_drop k n x x0 H8 t) H9)))) H7))) c2 H5))))
+H4)) (\lambda (H4: (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_:
+A).(eq K k (Bind Abst))))) (\lambda (c3: C).(\lambda (w: T).(\lambda (_:
+A).(eq C c2 (CHead c3 (Bind Abbr) w))))) (\lambda (c3: C).(\lambda (_:
+T).(\lambda (_: A).(csubc g c c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda
+(a: A).(sc3 g (asucc g a) c t)))) (\lambda (c3: C).(\lambda (w: T).(\lambda
+(a: A).(sc3 g a c3 w)))))).(ex5_3_ind C T A (\lambda (_: C).(\lambda (_:
+T).(\lambda (_: A).(eq K k (Bind Abst))))) (\lambda (c3: C).(\lambda (w:
+T).(\lambda (_: A).(eq C c2 (CHead c3 (Bind Abbr) w))))) (\lambda (c3:
+C).(\lambda (_: T).(\lambda (_: A).(csubc g c c3)))) (\lambda (_: C).(\lambda
+(_: T).(\lambda (a: A).(sc3 g (asucc g a) c t)))) (\lambda (c3: C).(\lambda
+(w: T).(\lambda (a: A).(sc3 g a c3 w)))) (ex2 C (\lambda (e2: C).(drop (S n)
+O c2 e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda (x0: C).(\lambda (x1:
+T).(\lambda (x2: A).(\lambda (H5: (eq K k (Bind Abst))).(\lambda (H6: (eq C
+c2 (CHead x0 (Bind Abbr) x1))).(\lambda (H7: (csubc g c x0)).(\lambda (_:
+(sc3 g (asucc g x2) c t)).(\lambda (_: (sc3 g x2 x0 x1)).(eq_ind_r C (CHead
+x0 (Bind Abbr) x1) (\lambda (c0: C).(ex2 C (\lambda (e2: C).(drop (S n) O c0
+e2)) (\lambda (e2: C).(csubc g e1 e2)))) (let H10 \def (eq_ind K k (\lambda
+(k0: K).(drop (r k0 n) O c e1)) (drop_gen_drop k c e1 t n H1) (Bind Abst) H5)
+in (let H11 \def (eq_ind K k (\lambda (k0: K).((drop n O (CHead c k0 t) e1)
+\to (\forall (c3: C).((csubc g (CHead c k0 t) c3) \to (ex2 C (\lambda (e2:
+C).(drop n O c3 e2)) (\lambda (e2: C).(csubc g e1 e2))))))) H0 (Bind Abst)
+H5) in (let H_x0 \def (H e1 (r (Bind Abst) n) H10 x0 H7) in (let H12 \def
+H_x0 in (ex2_ind C (\lambda (e2: C).(drop (r (Bind Abst) n) O x0 e2))
+(\lambda (e2: C).(csubc g e1 e2)) (ex2 C (\lambda (e2: C).(drop (S n) O
+(CHead x0 (Bind Abbr) x1) e2)) (\lambda (e2: C).(csubc g e1 e2))) (\lambda
+(x: C).(\lambda (H13: (drop (r (Bind Abst) n) O x0 x)).(\lambda (H14: (csubc
+g e1 x)).(ex_intro2 C (\lambda (e2: C).(drop (S n) O (CHead x0 (Bind Abbr)
+x1) e2)) (\lambda (e2: C).(csubc g e1 e2)) x (drop_drop (Bind Abbr) n x0 x
+H13 x1) H14)))) H12))))) c2 H6))))))))) H4)) H3)))))))) h))))))) c1)).
theorem drop_csubc_trans:
\forall (g: G).(\forall (c2: C).(\forall (e2: C).(\forall (d: nat).(\forall
x1) e3) \to (ex2 C (\lambda (c1: C).(drop h0 n c1 e3)) (\lambda (c1:
C).(csubc g (CHead c k t0) c1)))))))) H7 (lift h (r k n) x1) H4) in (eq_ind_r
T (lift h (r k n) x1) (\lambda (t0: T).(ex2 C (\lambda (c1: C).(drop h (S n)
-c1 e1)) (\lambda (c1: C).(csubc g (CHead c k t0) c1)))) (let H9 \def (match
-H6 in csubc return (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csubc ? c0
-c1)).((eq C c0 (CHead x0 k x1)) \to ((eq C c1 e1) \to (ex2 C (\lambda (c3:
-C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n)
-x1)) c3)))))))) with [(csubc_sort n0) \Rightarrow (\lambda (H9: (eq C (CSort
-n0) (CHead x0 k x1))).(\lambda (H10: (eq C (CSort n0) e1)).((let H11 \def
-(eq_ind C (CSort n0) (\lambda (e: C).(match e in C return (\lambda (_:
-C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
-False])) I (CHead x0 k x1) H9) in (False_ind ((eq C (CSort n0) e1) \to (ex2 C
-(\lambda (c1: C).(drop h (S n) c1 e1)) (\lambda (c1: C).(csubc g (CHead c k
-(lift h (r k n) x1)) c1)))) H11)) H10))) | (csubc_head c1 c0 H9 k0 v)
-\Rightarrow (\lambda (H10: (eq C (CHead c1 k0 v) (CHead x0 k x1))).(\lambda
-(H11: (eq C (CHead c0 k0 v) e1)).((let H12 \def (f_equal C T (\lambda (e:
-C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow v |
-(CHead _ _ t0) \Rightarrow t0])) (CHead c1 k0 v) (CHead x0 k x1) H10) in
-((let H13 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_:
-C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1]))
-(CHead c1 k0 v) (CHead x0 k x1) H10) in ((let H14 \def (f_equal C C (\lambda
-(e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c1
-| (CHead c3 _ _) \Rightarrow c3])) (CHead c1 k0 v) (CHead x0 k x1) H10) in
-(eq_ind C x0 (\lambda (c3: C).((eq K k0 k) \to ((eq T v x1) \to ((eq C (CHead
-c0 k0 v) e1) \to ((csubc g c3 c0) \to (ex2 C (\lambda (c4: C).(drop h (S n)
-c4 e1)) (\lambda (c4: C).(csubc g (CHead c k (lift h (r k n) x1)) c4))))))))
-(\lambda (H15: (eq K k0 k)).(eq_ind K k (\lambda (k1: K).((eq T v x1) \to
-((eq C (CHead c0 k1 v) e1) \to ((csubc g x0 c0) \to (ex2 C (\lambda (c3:
-C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n)
-x1)) c3))))))) (\lambda (H16: (eq T v x1)).(eq_ind T x1 (\lambda (t0: T).((eq
-C (CHead c0 k t0) e1) \to ((csubc g x0 c0) \to (ex2 C (\lambda (c3: C).(drop
-h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n) x1))
-c3)))))) (\lambda (H17: (eq C (CHead c0 k x1) e1)).(eq_ind C (CHead c0 k x1)
-(\lambda (c3: C).((csubc g x0 c0) \to (ex2 C (\lambda (c4: C).(drop h (S n)
-c4 c3)) (\lambda (c4: C).(csubc g (CHead c k (lift h (r k n) x1)) c4)))))
-(\lambda (H18: (csubc g x0 c0)).(let H_x \def (H x0 (r k n) h H5 c0 H18) in
-(let H19 \def H_x in (ex2_ind C (\lambda (c3: C).(drop h (r k n) c3 c0))
-(\lambda (c3: C).(csubc g c c3)) (ex2 C (\lambda (c3: C).(drop h (S n) c3
-(CHead c0 k x1))) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n) x1))
-c3))) (\lambda (x: C).(\lambda (H20: (drop h (r k n) x c0)).(\lambda (H21:
-(csubc g c x)).(ex_intro2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c0 k
-x1))) (\lambda (c3: C).(csubc g (CHead c k (lift h (r k n) x1)) c3)) (CHead x
-k (lift h (r k n) x1)) (drop_skip k h n x c0 H20 x1) (csubc_head g c x H21 k
-(lift h (r k n) x1)))))) H19)))) e1 H17)) v (sym_eq T v x1 H16))) k0 (sym_eq
-K k0 k H15))) c1 (sym_eq C c1 x0 H14))) H13)) H12)) H11 H9))) | (csubc_abst
-c1 c0 H9 v a H10 w H11) \Rightarrow (\lambda (H12: (eq C (CHead c1 (Bind
-Abst) v) (CHead x0 k x1))).(\lambda (H13: (eq C (CHead c0 (Bind Abbr) w)
-e1)).((let H14 \def (f_equal C T (\lambda (e: C).(match e in C return
-(\lambda (_: C).T) with [(CSort _) \Rightarrow v | (CHead _ _ t0) \Rightarrow
-t0])) (CHead c1 (Bind Abst) v) (CHead x0 k x1) H12) in ((let H15 \def
-(f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with
-[(CSort _) \Rightarrow (Bind Abst) | (CHead _ k0 _) \Rightarrow k0])) (CHead
-c1 (Bind Abst) v) (CHead x0 k x1) H12) in ((let H16 \def (f_equal C C
-(\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
-\Rightarrow c1 | (CHead c3 _ _) \Rightarrow c3])) (CHead c1 (Bind Abst) v)
-(CHead x0 k x1) H12) in (eq_ind C x0 (\lambda (c3: C).((eq K (Bind Abst) k)
-\to ((eq T v x1) \to ((eq C (CHead c0 (Bind Abbr) w) e1) \to ((csubc g c3 c0)
-\to ((sc3 g (asucc g a) c3 v) \to ((sc3 g a c0 w) \to (ex2 C (\lambda (c4:
-C).(drop h (S n) c4 e1)) (\lambda (c4: C).(csubc g (CHead c k (lift h (r k n)
-x1)) c4)))))))))) (\lambda (H17: (eq K (Bind Abst) k)).(eq_ind K (Bind Abst)
-(\lambda (k0: K).((eq T v x1) \to ((eq C (CHead c0 (Bind Abbr) w) e1) \to
-((csubc g x0 c0) \to ((sc3 g (asucc g a) x0 v) \to ((sc3 g a c0 w) \to (ex2 C
-(\lambda (c3: C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c k0
-(lift h (r k0 n) x1)) c3))))))))) (\lambda (H18: (eq T v x1)).(eq_ind T x1
-(\lambda (t0: T).((eq C (CHead c0 (Bind Abbr) w) e1) \to ((csubc g x0 c0) \to
-((sc3 g (asucc g a) x0 t0) \to ((sc3 g a c0 w) \to (ex2 C (\lambda (c3:
-C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g (CHead c (Bind Abst) (lift
-h (r (Bind Abst) n) x1)) c3)))))))) (\lambda (H19: (eq C (CHead c0 (Bind
-Abbr) w) e1)).(eq_ind C (CHead c0 (Bind Abbr) w) (\lambda (c3: C).((csubc g
-x0 c0) \to ((sc3 g (asucc g a) x0 x1) \to ((sc3 g a c0 w) \to (ex2 C (\lambda
-(c4: C).(drop h (S n) c4 c3)) (\lambda (c4: C).(csubc g (CHead c (Bind Abst)
-(lift h (r (Bind Abst) n) x1)) c4))))))) (\lambda (H20: (csubc g x0
-c0)).(\lambda (H21: (sc3 g (asucc g a) x0 x1)).(\lambda (H22: (sc3 g a c0
-w)).(let H23 \def (eq_ind_r K k (\lambda (k0: K).(\forall (h0: nat).((drop h0
-n (CHead c k0 (lift h (r k0 n) x1)) (CHead x0 k0 x1)) \to (\forall (e3:
-C).((csubc g (CHead x0 k0 x1) e3) \to (ex2 C (\lambda (c3: C).(drop h0 n c3
-e3)) (\lambda (c3: C).(csubc g (CHead c k0 (lift h (r k0 n) x1)) c3))))))))
-H8 (Bind Abst) H17) in (let H24 \def (eq_ind_r K k (\lambda (k0: K).(drop h
-(r k0 n) c x0)) H5 (Bind Abst) H17) in (let H_x \def (H x0 (r (Bind Abst) n)
-h H24 c0 H20) in (let H25 \def H_x in (ex2_ind C (\lambda (c3: C).(drop h (r
-(Bind Abst) n) c3 c0)) (\lambda (c3: C).(csubc g c c3)) (ex2 C (\lambda (c3:
-C).(drop h (S n) c3 (CHead c0 (Bind Abbr) w))) (\lambda (c3: C).(csubc g
-(CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1)) c3))) (\lambda (x:
-C).(\lambda (H26: (drop h (r (Bind Abst) n) x c0)).(\lambda (H27: (csubc g c
-x)).(ex_intro2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c0 (Bind Abbr) w)))
-(\lambda (c3: C).(csubc g (CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1))
-c3)) (CHead x (Bind Abbr) (lift h n w)) (drop_skip_bind h n x c0 H26 Abbr w)
-(csubc_abst g c x H27 (lift h (r (Bind Abst) n) x1) a (sc3_lift g (asucc g a)
-x0 x1 H21 c h (r (Bind Abst) n) H24) (lift h n w) (sc3_lift g a c0 w H22 x h
-n H26)))))) H25)))))))) e1 H19)) v (sym_eq T v x1 H18))) k H17)) c1 (sym_eq C
-c1 x0 H16))) H15)) H14)) H13 H9 H10 H11)))]) in (H9 (refl_equal C (CHead x0 k
-x1)) (refl_equal C e1))) t H4))))))))) (drop_gen_skip_l c e2 t h n k
+c1 e1)) (\lambda (c1: C).(csubc g (CHead c k t0) c1)))) (let H_x \def
+(csubc_gen_head_l g x0 e1 x1 k H6) in (let H9 \def H_x in (or_ind (ex2 C
+(\lambda (c3: C).(eq C e1 (CHead c3 k x1))) (\lambda (c3: C).(csubc g x0
+c3))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k
+(Bind Abst))))) (\lambda (c3: C).(\lambda (w: T).(\lambda (_: A).(eq C e1
+(CHead c3 (Bind Abbr) w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_:
+A).(csubc g x0 c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g
+(asucc g a) x0 x1)))) (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g
+a c3 w))))) (ex2 C (\lambda (c1: C).(drop h (S n) c1 e1)) (\lambda (c1:
+C).(csubc g (CHead c k (lift h (r k n) x1)) c1))) (\lambda (H10: (ex2 C
+(\lambda (c3: C).(eq C e1 (CHead c3 k x1))) (\lambda (c3: C).(csubc g x0
+c3)))).(ex2_ind C (\lambda (c3: C).(eq C e1 (CHead c3 k x1))) (\lambda (c3:
+C).(csubc g x0 c3)) (ex2 C (\lambda (c1: C).(drop h (S n) c1 e1)) (\lambda
+(c1: C).(csubc g (CHead c k (lift h (r k n) x1)) c1))) (\lambda (x:
+C).(\lambda (H11: (eq C e1 (CHead x k x1))).(\lambda (H12: (csubc g x0
+x)).(eq_ind_r C (CHead x k x1) (\lambda (c0: C).(ex2 C (\lambda (c1: C).(drop
+h (S n) c1 c0)) (\lambda (c1: C).(csubc g (CHead c k (lift h (r k n) x1))
+c1)))) (let H_x0 \def (H x0 (r k n) h H5 x H12) in (let H13 \def H_x0 in
+(ex2_ind C (\lambda (c1: C).(drop h (r k n) c1 x)) (\lambda (c1: C).(csubc g
+c c1)) (ex2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x k x1))) (\lambda
+(c1: C).(csubc g (CHead c k (lift h (r k n) x1)) c1))) (\lambda (x2:
+C).(\lambda (H14: (drop h (r k n) x2 x)).(\lambda (H15: (csubc g c
+x2)).(ex_intro2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x k x1))) (\lambda
+(c1: C).(csubc g (CHead c k (lift h (r k n) x1)) c1)) (CHead x2 k (lift h (r
+k n) x1)) (drop_skip k h n x2 x H14 x1) (csubc_head g c x2 H15 k (lift h (r k
+n) x1)))))) H13))) e1 H11)))) H10)) (\lambda (H10: (ex5_3 C T A (\lambda (_:
+C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst))))) (\lambda (c3:
+C).(\lambda (w: T).(\lambda (_: A).(eq C e1 (CHead c3 (Bind Abbr) w)))))
+(\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g x0 c3)))) (\lambda
+(_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) x0 x1)))) (\lambda
+(c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w)))))).(ex5_3_ind C T A
+(\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abst)))))
+(\lambda (c3: C).(\lambda (w: T).(\lambda (_: A).(eq C e1 (CHead c3 (Bind
+Abbr) w))))) (\lambda (c3: C).(\lambda (_: T).(\lambda (_: A).(csubc g x0
+c3)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g (asucc g a) x0
+x1)))) (\lambda (c3: C).(\lambda (w: T).(\lambda (a: A).(sc3 g a c3 w))))
+(ex2 C (\lambda (c1: C).(drop h (S n) c1 e1)) (\lambda (c1: C).(csubc g
+(CHead c k (lift h (r k n) x1)) c1))) (\lambda (x2: C).(\lambda (x3:
+T).(\lambda (x4: A).(\lambda (H11: (eq K k (Bind Abst))).(\lambda (H12: (eq C
+e1 (CHead x2 (Bind Abbr) x3))).(\lambda (H13: (csubc g x0 x2)).(\lambda (H14:
+(sc3 g (asucc g x4) x0 x1)).(\lambda (H15: (sc3 g x4 x2 x3)).(eq_ind_r C
+(CHead x2 (Bind Abbr) x3) (\lambda (c0: C).(ex2 C (\lambda (c1: C).(drop h (S
+n) c1 c0)) (\lambda (c1: C).(csubc g (CHead c k (lift h (r k n) x1)) c1))))
+(let H16 \def (eq_ind K k (\lambda (k0: K).(\forall (h0: nat).((drop h0 n
+(CHead c k0 (lift h (r k0 n) x1)) (CHead x0 k0 x1)) \to (\forall (e3:
+C).((csubc g (CHead x0 k0 x1) e3) \to (ex2 C (\lambda (c1: C).(drop h0 n c1
+e3)) (\lambda (c1: C).(csubc g (CHead c k0 (lift h (r k0 n) x1)) c1))))))))
+H8 (Bind Abst) H11) in (let H17 \def (eq_ind K k (\lambda (k0: K).(drop h (r
+k0 n) c x0)) H5 (Bind Abst) H11) in (eq_ind_r K (Bind Abst) (\lambda (k0:
+K).(ex2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x2 (Bind Abbr) x3)))
+(\lambda (c1: C).(csubc g (CHead c k0 (lift h (r k0 n) x1)) c1)))) (let H_x0
+\def (H x0 (r (Bind Abst) n) h H17 x2 H13) in (let H18 \def H_x0 in (ex2_ind
+C (\lambda (c1: C).(drop h (r (Bind Abst) n) c1 x2)) (\lambda (c1: C).(csubc
+g c c1)) (ex2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x2 (Bind Abbr) x3)))
+(\lambda (c1: C).(csubc g (CHead c (Bind Abst) (lift h (r (Bind Abst) n) x1))
+c1))) (\lambda (x: C).(\lambda (H19: (drop h (r (Bind Abst) n) x
+x2)).(\lambda (H20: (csubc g c x)).(ex_intro2 C (\lambda (c1: C).(drop h (S
+n) c1 (CHead x2 (Bind Abbr) x3))) (\lambda (c1: C).(csubc g (CHead c (Bind
+Abst) (lift h (r (Bind Abst) n) x1)) c1)) (CHead x (Bind Abbr) (lift h n x3))
+(drop_skip_bind h n x x2 H19 Abbr x3) (csubc_abst g c x H20 (lift h (r (Bind
+Abst) n) x1) x4 (sc3_lift g (asucc g x4) x0 x1 H14 c h (r (Bind Abst) n) H17)
+(lift h n x3) (sc3_lift g x4 x2 x3 H15 x h n H19)))))) H18))) k H11))) e1
+H12))))))))) H10)) H9))) t H4))))))))) (drop_gen_skip_l c e2 t h n k
H1)))))))) d))))))) c2)).
theorem csubc_drop_conf_rev:
k x1)) \to (ex2 C (\lambda (c1: C).(drop h0 n c1 e3)) (\lambda (c1: C).(csubc
g c1 (CHead c k t0))))))))) H7 (lift h (r k n) x1) H4) in (eq_ind_r T (lift h
(r k n) x1) (\lambda (t0: T).(ex2 C (\lambda (c1: C).(drop h (S n) c1 e1))
-(\lambda (c1: C).(csubc g c1 (CHead c k t0))))) (let H9 \def (match H6 in
-csubc return (\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (csubc ? c0
-c1)).((eq C c0 e1) \to ((eq C c1 (CHead x0 k x1)) \to (ex2 C (\lambda (c3:
-C).(drop h (S n) c3 e1)) (\lambda (c3: C).(csubc g c3 (CHead c k (lift h (r k
-n) x1)))))))))) with [(csubc_sort n0) \Rightarrow (\lambda (H9: (eq C (CSort
-n0) e1)).(\lambda (H10: (eq C (CSort n0) (CHead x0 k x1))).(eq_ind C (CSort
-n0) (\lambda (c0: C).((eq C (CSort n0) (CHead x0 k x1)) \to (ex2 C (\lambda
-(c1: C).(drop h (S n) c1 c0)) (\lambda (c1: C).(csubc g c1 (CHead c k (lift h
-(r k n) x1))))))) (\lambda (H11: (eq C (CSort n0) (CHead x0 k x1))).(let H12
-\def (eq_ind C (CSort n0) (\lambda (e: C).(match e in C return (\lambda (_:
-C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow
-False])) I (CHead x0 k x1) H11) in (False_ind (ex2 C (\lambda (c1: C).(drop h
-(S n) c1 (CSort n0))) (\lambda (c1: C).(csubc g c1 (CHead c k (lift h (r k n)
-x1))))) H12))) e1 H9 H10))) | (csubc_head c1 c0 H9 k0 v) \Rightarrow (\lambda
-(H10: (eq C (CHead c1 k0 v) e1)).(\lambda (H11: (eq C (CHead c0 k0 v) (CHead
-x0 k x1))).(eq_ind C (CHead c1 k0 v) (\lambda (c3: C).((eq C (CHead c0 k0 v)
-(CHead x0 k x1)) \to ((csubc g c1 c0) \to (ex2 C (\lambda (c4: C).(drop h (S
-n) c4 c3)) (\lambda (c4: C).(csubc g c4 (CHead c k (lift h (r k n) x1))))))))
-(\lambda (H12: (eq C (CHead c0 k0 v) (CHead x0 k x1))).(let H13 \def (f_equal
-C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
-\Rightarrow v | (CHead _ _ t0) \Rightarrow t0])) (CHead c0 k0 v) (CHead x0 k
-x1) H12) in ((let H14 \def (f_equal C K (\lambda (e: C).(match e in C return
-(\lambda (_: C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k1 _)
-\Rightarrow k1])) (CHead c0 k0 v) (CHead x0 k x1) H12) in ((let H15 \def
-(f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with
-[(CSort _) \Rightarrow c0 | (CHead c3 _ _) \Rightarrow c3])) (CHead c0 k0 v)
-(CHead x0 k x1) H12) in (eq_ind C x0 (\lambda (c3: C).((eq K k0 k) \to ((eq T
-v x1) \to ((csubc g c1 c3) \to (ex2 C (\lambda (c4: C).(drop h (S n) c4
-(CHead c1 k0 v))) (\lambda (c4: C).(csubc g c4 (CHead c k (lift h (r k n)
-x1))))))))) (\lambda (H16: (eq K k0 k)).(eq_ind K k (\lambda (k1: K).((eq T v
-x1) \to ((csubc g c1 x0) \to (ex2 C (\lambda (c3: C).(drop h (S n) c3 (CHead
-c1 k1 v))) (\lambda (c3: C).(csubc g c3 (CHead c k (lift h (r k n) x1))))))))
-(\lambda (H17: (eq T v x1)).(eq_ind T x1 (\lambda (t0: T).((csubc g c1 x0)
-\to (ex2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c1 k t0))) (\lambda (c3:
-C).(csubc g c3 (CHead c k (lift h (r k n) x1))))))) (\lambda (H18: (csubc g
-c1 x0)).(let H19 \def (eq_ind T v (\lambda (t0: T).(eq C (CHead c1 k0 t0)
-e1)) H10 x1 H17) in (let H20 \def (eq_ind K k0 (\lambda (k1: K).(eq C (CHead
-c1 k1 x1) e1)) H19 k H16) in (let H_x \def (H x0 (r k n) h H5 c1 H18) in (let
-H21 \def H_x in (ex2_ind C (\lambda (c3: C).(drop h (r k n) c3 c1)) (\lambda
-(c3: C).(csubc g c3 c)) (ex2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c1 k
-x1))) (\lambda (c3: C).(csubc g c3 (CHead c k (lift h (r k n) x1)))))
-(\lambda (x: C).(\lambda (H22: (drop h (r k n) x c1)).(\lambda (H23: (csubc g
-x c)).(ex_intro2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c1 k x1)))
-(\lambda (c3: C).(csubc g c3 (CHead c k (lift h (r k n) x1)))) (CHead x k
-(lift h (r k n) x1)) (drop_skip k h n x c1 H22 x1) (csubc_head g x c H23 k
-(lift h (r k n) x1)))))) H21)))))) v (sym_eq T v x1 H17))) k0 (sym_eq K k0 k
-H16))) c0 (sym_eq C c0 x0 H15))) H14)) H13))) e1 H10 H11 H9))) | (csubc_abst
-c1 c0 H9 v a H10 w H11) \Rightarrow (\lambda (H12: (eq C (CHead c1 (Bind
-Abst) v) e1)).(\lambda (H13: (eq C (CHead c0 (Bind Abbr) w) (CHead x0 k
-x1))).(eq_ind C (CHead c1 (Bind Abst) v) (\lambda (c3: C).((eq C (CHead c0
-(Bind Abbr) w) (CHead x0 k x1)) \to ((csubc g c1 c0) \to ((sc3 g (asucc g a)
-c1 v) \to ((sc3 g a c0 w) \to (ex2 C (\lambda (c4: C).(drop h (S n) c4 c3))
-(\lambda (c4: C).(csubc g c4 (CHead c k (lift h (r k n) x1)))))))))) (\lambda
-(H14: (eq C (CHead c0 (Bind Abbr) w) (CHead x0 k x1))).(let H15 \def (f_equal
-C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
-\Rightarrow w | (CHead _ _ t0) \Rightarrow t0])) (CHead c0 (Bind Abbr) w)
-(CHead x0 k x1) H14) in ((let H16 \def (f_equal C K (\lambda (e: C).(match e
-in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow (Bind Abbr) |
-(CHead _ k0 _) \Rightarrow k0])) (CHead c0 (Bind Abbr) w) (CHead x0 k x1)
-H14) in ((let H17 \def (f_equal C C (\lambda (e: C).(match e in C return
-(\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c3 _ _)
-\Rightarrow c3])) (CHead c0 (Bind Abbr) w) (CHead x0 k x1) H14) in (eq_ind C
-x0 (\lambda (c3: C).((eq K (Bind Abbr) k) \to ((eq T w x1) \to ((csubc g c1
-c3) \to ((sc3 g (asucc g a) c1 v) \to ((sc3 g a c3 w) \to (ex2 C (\lambda
-(c4: C).(drop h (S n) c4 (CHead c1 (Bind Abst) v))) (\lambda (c4: C).(csubc g
-c4 (CHead c k (lift h (r k n) x1))))))))))) (\lambda (H18: (eq K (Bind Abbr)
-k)).(eq_ind K (Bind Abbr) (\lambda (k0: K).((eq T w x1) \to ((csubc g c1 x0)
-\to ((sc3 g (asucc g a) c1 v) \to ((sc3 g a x0 w) \to (ex2 C (\lambda (c3:
-C).(drop h (S n) c3 (CHead c1 (Bind Abst) v))) (\lambda (c3: C).(csubc g c3
-(CHead c k0 (lift h (r k0 n) x1)))))))))) (\lambda (H19: (eq T w x1)).(eq_ind
-T x1 (\lambda (t0: T).((csubc g c1 x0) \to ((sc3 g (asucc g a) c1 v) \to
-((sc3 g a x0 t0) \to (ex2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c1 (Bind
-Abst) v))) (\lambda (c3: C).(csubc g c3 (CHead c (Bind Abbr) (lift h (r (Bind
-Abbr) n) x1))))))))) (\lambda (H20: (csubc g c1 x0)).(\lambda (H21: (sc3 g
-(asucc g a) c1 v)).(\lambda (H22: (sc3 g a x0 x1)).(let H23 \def (eq_ind_r K
-k (\lambda (k0: K).(\forall (h0: nat).((drop h0 n (CHead c k0 (lift h (r k0
-n) x1)) (CHead x0 k0 x1)) \to (\forall (e3: C).((csubc g e3 (CHead x0 k0 x1))
-\to (ex2 C (\lambda (c3: C).(drop h0 n c3 e3)) (\lambda (c3: C).(csubc g c3
-(CHead c k0 (lift h (r k0 n) x1)))))))))) H8 (Bind Abbr) H18) in (let H24
-\def (eq_ind_r K k (\lambda (k0: K).(drop h (r k0 n) c x0)) H5 (Bind Abbr)
-H18) in (let H_x \def (H x0 (r (Bind Abbr) n) h H24 c1 H20) in (let H25 \def
-H_x in (ex2_ind C (\lambda (c3: C).(drop h (r (Bind Abbr) n) c3 c1)) (\lambda
-(c3: C).(csubc g c3 c)) (ex2 C (\lambda (c3: C).(drop h (S n) c3 (CHead c1
-(Bind Abst) v))) (\lambda (c3: C).(csubc g c3 (CHead c (Bind Abbr) (lift h (r
-(Bind Abbr) n) x1))))) (\lambda (x: C).(\lambda (H26: (drop h (r (Bind Abbr)
-n) x c1)).(\lambda (H27: (csubc g x c)).(ex_intro2 C (\lambda (c3: C).(drop h
-(S n) c3 (CHead c1 (Bind Abst) v))) (\lambda (c3: C).(csubc g c3 (CHead c
-(Bind Abbr) (lift h (r (Bind Abbr) n) x1)))) (CHead x (Bind Abst) (lift h n
-v)) (drop_skip_bind h n x c1 H26 Abst v) (csubc_abst g x c H27 (lift h n v) a
-(sc3_lift g (asucc g a) c1 v H21 x h n H26) (lift h (r (Bind Abbr) n) x1)
-(sc3_lift g a x0 x1 H22 c h (r (Bind Abbr) n) H24)))))) H25)))))))) w (sym_eq
-T w x1 H19))) k H18)) c0 (sym_eq C c0 x0 H17))) H16)) H15))) e1 H12 H13 H9
-H10 H11)))]) in (H9 (refl_equal C e1) (refl_equal C (CHead x0 k x1)))) t
-H4))))))))) (drop_gen_skip_l c e2 t h n k H1)))))))) d))))))) c2)).
+(\lambda (c1: C).(csubc g c1 (CHead c k t0))))) (let H_x \def
+(csubc_gen_head_r g x0 e1 x1 k H6) in (let H9 \def H_x in (or_ind (ex2 C
+(\lambda (c1: C).(eq C e1 (CHead c1 k x1))) (\lambda (c1: C).(csubc g c1
+x0))) (ex5_3 C T A (\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k
+(Bind Abbr))))) (\lambda (c1: C).(\lambda (v: T).(\lambda (_: A).(eq C e1
+(CHead c1 (Bind Abst) v))))) (\lambda (c1: C).(\lambda (_: T).(\lambda (_:
+A).(csubc g c1 x0)))) (\lambda (c1: C).(\lambda (v: T).(\lambda (a: A).(sc3 g
+(asucc g a) c1 v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a
+x0 x1))))) (ex2 C (\lambda (c1: C).(drop h (S n) c1 e1)) (\lambda (c1:
+C).(csubc g c1 (CHead c k (lift h (r k n) x1))))) (\lambda (H10: (ex2 C
+(\lambda (c1: C).(eq C e1 (CHead c1 k x1))) (\lambda (c1: C).(csubc g c1
+x0)))).(ex2_ind C (\lambda (c1: C).(eq C e1 (CHead c1 k x1))) (\lambda (c1:
+C).(csubc g c1 x0)) (ex2 C (\lambda (c1: C).(drop h (S n) c1 e1)) (\lambda
+(c1: C).(csubc g c1 (CHead c k (lift h (r k n) x1))))) (\lambda (x:
+C).(\lambda (H11: (eq C e1 (CHead x k x1))).(\lambda (H12: (csubc g x
+x0)).(eq_ind_r C (CHead x k x1) (\lambda (c0: C).(ex2 C (\lambda (c1:
+C).(drop h (S n) c1 c0)) (\lambda (c1: C).(csubc g c1 (CHead c k (lift h (r k
+n) x1)))))) (let H_x0 \def (H x0 (r k n) h H5 x H12) in (let H13 \def H_x0 in
+(ex2_ind C (\lambda (c1: C).(drop h (r k n) c1 x)) (\lambda (c1: C).(csubc g
+c1 c)) (ex2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x k x1))) (\lambda
+(c1: C).(csubc g c1 (CHead c k (lift h (r k n) x1))))) (\lambda (x2:
+C).(\lambda (H14: (drop h (r k n) x2 x)).(\lambda (H15: (csubc g x2
+c)).(ex_intro2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x k x1))) (\lambda
+(c1: C).(csubc g c1 (CHead c k (lift h (r k n) x1)))) (CHead x2 k (lift h (r
+k n) x1)) (drop_skip k h n x2 x H14 x1) (csubc_head g x2 c H15 k (lift h (r k
+n) x1)))))) H13))) e1 H11)))) H10)) (\lambda (H10: (ex5_3 C T A (\lambda (_:
+C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr))))) (\lambda (c1:
+C).(\lambda (v: T).(\lambda (_: A).(eq C e1 (CHead c1 (Bind Abst) v)))))
+(\lambda (c1: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1 x0)))) (\lambda
+(c1: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c1 v)))) (\lambda
+(_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a x0 x1)))))).(ex5_3_ind C T A
+(\lambda (_: C).(\lambda (_: T).(\lambda (_: A).(eq K k (Bind Abbr)))))
+(\lambda (c1: C).(\lambda (v: T).(\lambda (_: A).(eq C e1 (CHead c1 (Bind
+Abst) v))))) (\lambda (c1: C).(\lambda (_: T).(\lambda (_: A).(csubc g c1
+x0)))) (\lambda (c1: C).(\lambda (v: T).(\lambda (a: A).(sc3 g (asucc g a) c1
+v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(sc3 g a x0 x1)))) (ex2
+C (\lambda (c1: C).(drop h (S n) c1 e1)) (\lambda (c1: C).(csubc g c1 (CHead
+c k (lift h (r k n) x1))))) (\lambda (x2: C).(\lambda (x3: T).(\lambda (x4:
+A).(\lambda (H11: (eq K k (Bind Abbr))).(\lambda (H12: (eq C e1 (CHead x2
+(Bind Abst) x3))).(\lambda (H13: (csubc g x2 x0)).(\lambda (H14: (sc3 g
+(asucc g x4) x2 x3)).(\lambda (H15: (sc3 g x4 x0 x1)).(eq_ind_r C (CHead x2
+(Bind Abst) x3) (\lambda (c0: C).(ex2 C (\lambda (c1: C).(drop h (S n) c1
+c0)) (\lambda (c1: C).(csubc g c1 (CHead c k (lift h (r k n) x1)))))) (let
+H16 \def (eq_ind K k (\lambda (k0: K).(\forall (h0: nat).((drop h0 n (CHead c
+k0 (lift h (r k0 n) x1)) (CHead x0 k0 x1)) \to (\forall (e3: C).((csubc g e3
+(CHead x0 k0 x1)) \to (ex2 C (\lambda (c1: C).(drop h0 n c1 e3)) (\lambda
+(c1: C).(csubc g c1 (CHead c k0 (lift h (r k0 n) x1)))))))))) H8 (Bind Abbr)
+H11) in (let H17 \def (eq_ind K k (\lambda (k0: K).(drop h (r k0 n) c x0)) H5
+(Bind Abbr) H11) in (eq_ind_r K (Bind Abbr) (\lambda (k0: K).(ex2 C (\lambda
+(c1: C).(drop h (S n) c1 (CHead x2 (Bind Abst) x3))) (\lambda (c1: C).(csubc
+g c1 (CHead c k0 (lift h (r k0 n) x1)))))) (let H_x0 \def (H x0 (r (Bind
+Abbr) n) h H17 x2 H13) in (let H18 \def H_x0 in (ex2_ind C (\lambda (c1:
+C).(drop h (r (Bind Abbr) n) c1 x2)) (\lambda (c1: C).(csubc g c1 c)) (ex2 C
+(\lambda (c1: C).(drop h (S n) c1 (CHead x2 (Bind Abst) x3))) (\lambda (c1:
+C).(csubc g c1 (CHead c (Bind Abbr) (lift h (r (Bind Abbr) n) x1)))))
+(\lambda (x: C).(\lambda (H19: (drop h (r (Bind Abbr) n) x x2)).(\lambda
+(H20: (csubc g x c)).(ex_intro2 C (\lambda (c1: C).(drop h (S n) c1 (CHead x2
+(Bind Abst) x3))) (\lambda (c1: C).(csubc g c1 (CHead c (Bind Abbr) (lift h
+(r (Bind Abbr) n) x1)))) (CHead x (Bind Abst) (lift h n x3)) (drop_skip_bind
+h n x x2 H19 Abst x3) (csubc_abst g x c H20 (lift h n x3) x4 (sc3_lift g
+(asucc g x4) x2 x3 H14 x h n H19) (lift h (r (Bind Abbr) n) x1) (sc3_lift g
+x4 x0 x1 H15 c h (r (Bind Abbr) n) H17)))))) H18))) k H11))) e1 H12)))))))))
+H10)) H9))) t H4))))))))) (drop_gen_skip_l c e2 t h n k H1)))))))) d)))))))
+c2)).
projects / helm.git / blobdiff