a)))))))))) (\lambda (a: C).(\lambda (c: C).(\lambda (H: (drop O O c
a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H0: (drop h
d c e)).(\lambda (H1: (le (plus d h) O)).(let H2 \def (eq_ind C c (\lambda
-(c0: C).(drop h d c0 e)) H0 a (drop_gen_refl c a H)) in (let H3 \def (match
-H1 in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) \to
-(drop (minus O h) O e a)))) with [le_n \Rightarrow (\lambda (H3: (eq nat
-(plus d h) O)).(let H4 \def (f_equal nat nat (\lambda (e0: nat).e0) (plus d
-h) O H3) in (eq_ind nat (plus d h) (\lambda (n: nat).(drop (minus n h) n e
-a)) (eq_ind_r nat O (\lambda (n: nat).(drop (minus n h) n e a)) (and_ind (eq
-nat d O) (eq nat h O) (drop O O e a) (\lambda (H5: (eq nat d O)).(\lambda
-(H6: (eq nat h O)).(let H7 \def (eq_ind nat d (\lambda (n: nat).(drop h n a
-e)) H2 O H5) in (let H8 \def (eq_ind nat h (\lambda (n: nat).(drop n O a e))
-H7 O H6) in (eq_ind C a (\lambda (c0: C).(drop O O c0 a)) (drop_refl a) e
-(drop_gen_refl a e H8)))))) (plus_O d h H4)) (plus d h) H4) O H4))) | (le_S m
-H3) \Rightarrow (\lambda (H4: (eq nat (S m) O)).((let H5 \def (eq_ind nat (S
-m) (\lambda (e0: nat).(match e0 in nat return (\lambda (_: nat).Prop) with [O
-\Rightarrow False | (S _) \Rightarrow True])) I O H4) in (False_ind ((le
-(plus d h) m) \to (drop (minus O h) O e a)) H5)) H3))]) in (H3 (refl_equal
-nat O)))))))))))) (\lambda (i0: nat).(\lambda (H: ((\forall (a: C).(\forall
-(c: C).((drop i0 O c a) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
-nat).((drop h d c e) \to ((le (plus d h) i0) \to (drop (minus i0 h) O e
-a))))))))))).(\lambda (a: C).(\lambda (c: C).(C_ind (\lambda (c0: C).((drop
-(S i0) O c0 a) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop
-h d c0 e) \to ((le (plus d h) (S i0)) \to (drop (minus (S i0) h) O e
-a)))))))) (\lambda (n: nat).(\lambda (H0: (drop (S i0) O (CSort n)
-a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (drop h
-d (CSort n) e)).(\lambda (H2: (le (plus d h) (S i0))).(and3_ind (eq C e
-(CSort n)) (eq nat h O) (eq nat d O) (drop (minus (S i0) h) O e a) (\lambda
-(H3: (eq C e (CSort n))).(\lambda (H4: (eq nat h O)).(\lambda (H5: (eq nat d
-O)).(and3_ind (eq C a (CSort n)) (eq nat (S i0) O) (eq nat O O) (drop (minus
-(S i0) h) O e a) (\lambda (H6: (eq C a (CSort n))).(\lambda (H7: (eq nat (S
-i0) O)).(\lambda (_: (eq nat O O)).(let H9 \def (eq_ind nat d (\lambda (n0:
-nat).(le (plus n0 h) (S i0))) H2 O H5) in (let H10 \def (eq_ind nat h
-(\lambda (n0: nat).(le (plus O n0) (S i0))) H9 O H4) in (eq_ind_r nat O
-(\lambda (n0: nat).(drop (minus (S i0) n0) O e a)) (eq_ind_r C (CSort n)
-(\lambda (c0: C).(drop (minus (S i0) O) O c0 a)) (eq_ind_r C (CSort n)
-(\lambda (c0: C).(drop (minus (S i0) O) O (CSort n) c0)) (let H11 \def
-(eq_ind nat (S i0) (\lambda (ee: nat).(match ee in nat return (\lambda (_:
-nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H7) in
-(False_ind (drop (minus (S i0) O) O (CSort n) (CSort n)) H11)) a H6) e H3) h
-H4)))))) (drop_gen_sort n (S i0) O a H0))))) (drop_gen_sort n h d e
-H1))))))))) (\lambda (c0: C).(\lambda (H0: (((drop (S i0) O c0 a) \to
-(\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c0 e) \to ((le
-(plus d h) (S i0)) \to (drop (minus (S i0) h) O e a))))))))).(\lambda (k:
-K).(K_ind (\lambda (k0: K).(\forall (t: T).((drop (S i0) O (CHead c0 k0 t) a)
-\to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d (CHead c0
-k0 t) e) \to ((le (plus d h) (S i0)) \to (drop (minus (S i0) h) O e
-a))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (H1: (drop (S i0) O
-(CHead c0 (Bind b) t) a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d:
-nat).(\lambda (H2: (drop h d (CHead c0 (Bind b) t) e)).(\lambda (H3: (le
-(plus d h) (S i0))).(nat_ind (\lambda (n: nat).((drop h n (CHead c0 (Bind b)
-t) e) \to ((le (plus n h) (S i0)) \to (drop (minus (S i0) h) O e a))))
-(\lambda (H4: (drop h O (CHead c0 (Bind b) t) e)).(\lambda (H5: (le (plus O
-h) (S i0))).(nat_ind (\lambda (n: nat).((drop n O (CHead c0 (Bind b) t) e)
-\to ((le (plus O n) (S i0)) \to (drop (minus (S i0) n) O e a)))) (\lambda
-(H6: (drop O O (CHead c0 (Bind b) t) e)).(\lambda (_: (le (plus O O) (S
-i0))).(eq_ind C (CHead c0 (Bind b) t) (\lambda (c1: C).(drop (minus (S i0) O)
-O c1 a)) (drop_drop (Bind b) i0 c0 a (drop_gen_drop (Bind b) c0 a t i0 H1) t)
-e (drop_gen_refl (CHead c0 (Bind b) t) e H6)))) (\lambda (h0: nat).(\lambda
-(_: (((drop h0 O (CHead c0 (Bind b) t) e) \to ((le (plus O h0) (S i0)) \to
-(drop (minus (S i0) h0) O e a))))).(\lambda (H6: (drop (S h0) O (CHead c0
-(Bind b) t) e)).(\lambda (H7: (le (plus O (S h0)) (S i0))).(H a c0
-(drop_gen_drop (Bind b) c0 a t i0 H1) e h0 O (drop_gen_drop (Bind b) c0 e t
-h0 H6) (le_S_n (plus O h0) i0 H7)))))) h H4 H5))) (\lambda (d0: nat).(\lambda
-(_: (((drop h d0 (CHead c0 (Bind b) t) e) \to ((le (plus d0 h) (S i0)) \to
-(drop (minus (S i0) h) O e a))))).(\lambda (H4: (drop h (S d0) (CHead c0
-(Bind b) t) e)).(\lambda (H5: (le (plus (S d0) h) (S i0))).(ex3_2_ind C T
-(\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 (Bind b) v)))) (\lambda
-(_: C).(\lambda (v: T).(eq T t (lift h (r (Bind b) d0) v)))) (\lambda (e0:
-C).(\lambda (_: T).(drop h (r (Bind b) d0) c0 e0))) (drop (minus (S i0) h) O
-e a) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C e (CHead x0 (Bind
-b) x1))).(\lambda (_: (eq T t (lift h (r (Bind b) d0) x1))).(\lambda (H8:
-(drop h (r (Bind b) d0) c0 x0)).(eq_ind_r C (CHead x0 (Bind b) x1) (\lambda
-(c1: C).(drop (minus (S i0) h) O c1 a)) (eq_ind nat (S (minus i0 h)) (\lambda
-(n: nat).(drop n O (CHead x0 (Bind b) x1) a)) (drop_drop (Bind b) (minus i0
-h) x0 a (H a c0 (drop_gen_drop (Bind b) c0 a t i0 H1) x0 h d0 H8 (le_S_n
-(plus d0 h) i0 H5)) x1) (minus (S i0) h) (minus_Sn_m i0 h (le_trans_plus_r d0
-h i0 (le_S_n (plus d0 h) i0 H5)))) e H6)))))) (drop_gen_skip_l c0 e t h d0
-(Bind b) H4)))))) d H2 H3))))))))) (\lambda (f: F).(\lambda (t: T).(\lambda
-(H1: (drop (S i0) O (CHead c0 (Flat f) t) a)).(\lambda (e: C).(\lambda (h:
-nat).(\lambda (d: nat).(\lambda (H2: (drop h d (CHead c0 (Flat f) t)
+(c0: C).(drop h d c0 e)) H0 a (drop_gen_refl c a H)) in (let H_y \def
+(le_n_O_eq (plus d h) H1) in (land_ind (eq nat d O) (eq nat h O) (drop (minus
+O h) O e a) (\lambda (H3: (eq nat d O)).(\lambda (H4: (eq nat h O)).(let H5
+\def (eq_ind nat d (\lambda (n: nat).(drop h n a e)) H2 O H3) in (let H6 \def
+(eq_ind nat h (\lambda (n: nat).(drop n O a e)) H5 O H4) in (eq_ind_r nat O
+(\lambda (n: nat).(drop (minus O n) O e a)) (eq_ind C a (\lambda (c0:
+C).(drop (minus O O) O c0 a)) (drop_refl a) e (drop_gen_refl a e H6)) h
+H4))))) (plus_O d h (sym_eq nat O (plus d h) H_y))))))))))))) (\lambda (i0:
+nat).(\lambda (H: ((\forall (a: C).(\forall (c: C).((drop i0 O c a) \to
+(\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c e) \to ((le
+(plus d h) i0) \to (drop (minus i0 h) O e a))))))))))).(\lambda (a:
+C).(\lambda (c: C).(C_ind (\lambda (c0: C).((drop (S i0) O c0 a) \to (\forall
+(e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c0 e) \to ((le (plus d
+h) (S i0)) \to (drop (minus (S i0) h) O e a)))))))) (\lambda (n:
+nat).(\lambda (H0: (drop (S i0) O (CSort n) a)).(\lambda (e: C).(\lambda (h:
+nat).(\lambda (d: nat).(\lambda (H1: (drop h d (CSort n) e)).(\lambda (H2:
+(le (plus d h) (S i0))).(and3_ind (eq C e (CSort n)) (eq nat h O) (eq nat d
+O) (drop (minus (S i0) h) O e a) (\lambda (H3: (eq C e (CSort n))).(\lambda
+(H4: (eq nat h O)).(\lambda (H5: (eq nat d O)).(and3_ind (eq C a (CSort n))
+(eq nat (S i0) O) (eq nat O O) (drop (minus (S i0) h) O e a) (\lambda (H6:
+(eq C a (CSort n))).(\lambda (H7: (eq nat (S i0) O)).(\lambda (_: (eq nat O
+O)).(let H9 \def (eq_ind nat d (\lambda (n0: nat).(le (plus n0 h) (S i0))) H2
+O H5) in (let H10 \def (eq_ind nat h (\lambda (n0: nat).(le (plus O n0) (S
+i0))) H9 O H4) in (eq_ind_r nat O (\lambda (n0: nat).(drop (minus (S i0) n0)
+O e a)) (eq_ind_r C (CSort n) (\lambda (c0: C).(drop (minus (S i0) O) O c0
+a)) (eq_ind_r C (CSort n) (\lambda (c0: C).(drop (minus (S i0) O) O (CSort n)
+c0)) (let H11 \def (eq_ind nat (S i0) (\lambda (ee: nat).(match ee in nat
+return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
+True])) I O H7) in (False_ind (drop (minus (S i0) O) O (CSort n) (CSort n))
+H11)) a H6) e H3) h H4)))))) (drop_gen_sort n (S i0) O a H0)))))
+(drop_gen_sort n h d e H1))))))))) (\lambda (c0: C).(\lambda (H0: (((drop (S
+i0) O c0 a) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h
+d c0 e) \to ((le (plus d h) (S i0)) \to (drop (minus (S i0) h) O e
+a))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t: T).((drop (S
+i0) O (CHead c0 k0 t) a) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
+nat).((drop h d (CHead c0 k0 t) e) \to ((le (plus d h) (S i0)) \to (drop
+(minus (S i0) h) O e a))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (H1:
+(drop (S i0) O (CHead c0 (Bind b) t) a)).(\lambda (e: C).(\lambda (h:
+nat).(\lambda (d: nat).(\lambda (H2: (drop h d (CHead c0 (Bind b) t)
e)).(\lambda (H3: (le (plus d h) (S i0))).(nat_ind (\lambda (n: nat).((drop h
-n (CHead c0 (Flat f) t) e) \to ((le (plus n h) (S i0)) \to (drop (minus (S
-i0) h) O e a)))) (\lambda (H4: (drop h O (CHead c0 (Flat f) t) e)).(\lambda
+n (CHead c0 (Bind b) t) e) \to ((le (plus n h) (S i0)) \to (drop (minus (S
+i0) h) O e a)))) (\lambda (H4: (drop h O (CHead c0 (Bind b) t) e)).(\lambda
(H5: (le (plus O h) (S i0))).(nat_ind (\lambda (n: nat).((drop n O (CHead c0
-(Flat f) t) e) \to ((le (plus O n) (S i0)) \to (drop (minus (S i0) n) O e
-a)))) (\lambda (H6: (drop O O (CHead c0 (Flat f) t) e)).(\lambda (_: (le
-(plus O O) (S i0))).(eq_ind C (CHead c0 (Flat f) t) (\lambda (c1: C).(drop
-(minus (S i0) O) O c1 a)) (drop_drop (Flat f) i0 c0 a (drop_gen_drop (Flat f)
-c0 a t i0 H1) t) e (drop_gen_refl (CHead c0 (Flat f) t) e H6)))) (\lambda
-(h0: nat).(\lambda (_: (((drop h0 O (CHead c0 (Flat f) t) e) \to ((le (plus O
+(Bind b) t) e) \to ((le (plus O n) (S i0)) \to (drop (minus (S i0) n) O e
+a)))) (\lambda (H6: (drop O O (CHead c0 (Bind b) t) e)).(\lambda (_: (le
+(plus O O) (S i0))).(eq_ind C (CHead c0 (Bind b) t) (\lambda (c1: C).(drop
+(minus (S i0) O) O c1 a)) (drop_drop (Bind b) i0 c0 a (drop_gen_drop (Bind b)
+c0 a t i0 H1) t) e (drop_gen_refl (CHead c0 (Bind b) t) e H6)))) (\lambda
+(h0: nat).(\lambda (_: (((drop h0 O (CHead c0 (Bind b) t) e) \to ((le (plus O
h0) (S i0)) \to (drop (minus (S i0) h0) O e a))))).(\lambda (H6: (drop (S h0)
-O (CHead c0 (Flat f) t) e)).(\lambda (H7: (le (plus O (S h0)) (S i0))).(H0
-(drop_gen_drop (Flat f) c0 a t i0 H1) e (S h0) O (drop_gen_drop (Flat f) c0 e
-t h0 H6) H7))))) h H4 H5))) (\lambda (d0: nat).(\lambda (_: (((drop h d0
-(CHead c0 (Flat f) t) e) \to ((le (plus d0 h) (S i0)) \to (drop (minus (S i0)
-h) O e a))))).(\lambda (H4: (drop h (S d0) (CHead c0 (Flat f) t) e)).(\lambda
-(H5: (le (plus (S d0) h) (S i0))).(ex3_2_ind C T (\lambda (e0: C).(\lambda
-(v: T).(eq C e (CHead e0 (Flat f) v)))) (\lambda (_: C).(\lambda (v: T).(eq T
-t (lift h (r (Flat f) d0) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r
-(Flat f) d0) c0 e0))) (drop (minus (S i0) h) O e a) (\lambda (x0: C).(\lambda
-(x1: T).(\lambda (H6: (eq C e (CHead x0 (Flat f) x1))).(\lambda (_: (eq T t
-(lift h (r (Flat f) d0) x1))).(\lambda (H8: (drop h (r (Flat f) d0) c0
-x0)).(eq_ind_r C (CHead x0 (Flat f) x1) (\lambda (c1: C).(drop (minus (S i0)
-h) O c1 a)) (let H9 \def (eq_ind_r nat (minus (S i0) h) (\lambda (n:
-nat).(drop n O x0 a)) (H0 (drop_gen_drop (Flat f) c0 a t i0 H1) x0 h (S d0)
-H8 H5) (S (minus i0 h)) (minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n
-(plus d0 h) i0 H5)))) in (eq_ind nat (S (minus i0 h)) (\lambda (n: nat).(drop
-n O (CHead x0 (Flat f) x1) a)) (drop_drop (Flat f) (minus i0 h) x0 a H9 x1)
-(minus (S i0) h) (minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0
-h) i0 H5))))) e H6)))))) (drop_gen_skip_l c0 e t h d0 (Flat f) H4)))))) d H2
-H3))))))))) k)))) c))))) i).
+O (CHead c0 (Bind b) t) e)).(\lambda (H7: (le (plus O (S h0)) (S i0))).(H a
+c0 (drop_gen_drop (Bind b) c0 a t i0 H1) e h0 O (drop_gen_drop (Bind b) c0 e
+t h0 H6) (le_S_n (plus O h0) i0 H7)))))) h H4 H5))) (\lambda (d0:
+nat).(\lambda (_: (((drop h d0 (CHead c0 (Bind b) t) e) \to ((le (plus d0 h)
+(S i0)) \to (drop (minus (S i0) h) O e a))))).(\lambda (H4: (drop h (S d0)
+(CHead c0 (Bind b) t) e)).(\lambda (H5: (le (plus (S d0) h) (S
+i0))).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 (Bind
+b) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r (Bind b) d0)
+v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r (Bind b) d0) c0 e0))) (drop
+(minus (S i0) h) O e a) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C
+e (CHead x0 (Bind b) x1))).(\lambda (_: (eq T t (lift h (r (Bind b) d0)
+x1))).(\lambda (H8: (drop h (r (Bind b) d0) c0 x0)).(eq_ind_r C (CHead x0
+(Bind b) x1) (\lambda (c1: C).(drop (minus (S i0) h) O c1 a)) (eq_ind nat (S
+(minus i0 h)) (\lambda (n: nat).(drop n O (CHead x0 (Bind b) x1) a))
+(drop_drop (Bind b) (minus i0 h) x0 a (H a c0 (drop_gen_drop (Bind b) c0 a t
+i0 H1) x0 h d0 H8 (le_S_n (plus d0 h) i0 H5)) x1) (minus (S i0) h)
+(minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0 h) i0 H5)))) e
+H6)))))) (drop_gen_skip_l c0 e t h d0 (Bind b) H4)))))) d H2 H3)))))))))
+(\lambda (f: F).(\lambda (t: T).(\lambda (H1: (drop (S i0) O (CHead c0 (Flat
+f) t) a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H2:
+(drop h d (CHead c0 (Flat f) t) e)).(\lambda (H3: (le (plus d h) (S
+i0))).(nat_ind (\lambda (n: nat).((drop h n (CHead c0 (Flat f) t) e) \to ((le
+(plus n h) (S i0)) \to (drop (minus (S i0) h) O e a)))) (\lambda (H4: (drop h
+O (CHead c0 (Flat f) t) e)).(\lambda (H5: (le (plus O h) (S i0))).(nat_ind
+(\lambda (n: nat).((drop n O (CHead c0 (Flat f) t) e) \to ((le (plus O n) (S
+i0)) \to (drop (minus (S i0) n) O e a)))) (\lambda (H6: (drop O O (CHead c0
+(Flat f) t) e)).(\lambda (_: (le (plus O O) (S i0))).(eq_ind C (CHead c0
+(Flat f) t) (\lambda (c1: C).(drop (minus (S i0) O) O c1 a)) (drop_drop (Flat
+f) i0 c0 a (drop_gen_drop (Flat f) c0 a t i0 H1) t) e (drop_gen_refl (CHead
+c0 (Flat f) t) e H6)))) (\lambda (h0: nat).(\lambda (_: (((drop h0 O (CHead
+c0 (Flat f) t) e) \to ((le (plus O h0) (S i0)) \to (drop (minus (S i0) h0) O
+e a))))).(\lambda (H6: (drop (S h0) O (CHead c0 (Flat f) t) e)).(\lambda (H7:
+(le (plus O (S h0)) (S i0))).(H0 (drop_gen_drop (Flat f) c0 a t i0 H1) e (S
+h0) O (drop_gen_drop (Flat f) c0 e t h0 H6) H7))))) h H4 H5))) (\lambda (d0:
+nat).(\lambda (_: (((drop h d0 (CHead c0 (Flat f) t) e) \to ((le (plus d0 h)
+(S i0)) \to (drop (minus (S i0) h) O e a))))).(\lambda (H4: (drop h (S d0)
+(CHead c0 (Flat f) t) e)).(\lambda (H5: (le (plus (S d0) h) (S
+i0))).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 (Flat
+f) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r (Flat f) d0)
+v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r (Flat f) d0) c0 e0))) (drop
+(minus (S i0) h) O e a) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C
+e (CHead x0 (Flat f) x1))).(\lambda (_: (eq T t (lift h (r (Flat f) d0)
+x1))).(\lambda (H8: (drop h (r (Flat f) d0) c0 x0)).(eq_ind_r C (CHead x0
+(Flat f) x1) (\lambda (c1: C).(drop (minus (S i0) h) O c1 a)) (let H9 \def
+(eq_ind_r nat (minus (S i0) h) (\lambda (n: nat).(drop n O x0 a)) (H0
+(drop_gen_drop (Flat f) c0 a t i0 H1) x0 h (S d0) H8 H5) (S (minus i0 h))
+(minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0 h) i0 H5)))) in
+(eq_ind nat (S (minus i0 h)) (\lambda (n: nat).(drop n O (CHead x0 (Flat f)
+x1) a)) (drop_drop (Flat f) (minus i0 h) x0 a H9 x1) (minus (S i0) h)
+(minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0 h) i0 H5))))) e
+H6)))))) (drop_gen_skip_l c0 e t h d0 (Flat f) H4)))))) d H2 H3)))))))))
+k)))) c))))) i).
theorem drop_conf_rev:
\forall (j: nat).(\forall (e1: C).(\forall (e2: C).((drop j O e1 e2) \to
c2 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1:
C).(drop h (minus n (S i0)) e1 e2))))))))))) (\lambda (H: (le (S i0)
O)).(\lambda (c1: C).(\lambda (c2: C).(\lambda (h: nat).(\lambda (_: (drop h
-O c1 c2)).(\lambda (e2: C).(\lambda (_: (drop (S i0) O c2 e2)).(let H2 \def
-(match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O)
-\to (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1: C).(drop h
-(minus O (S i0)) e1 e2)))))) with [le_n \Rightarrow (\lambda (H2: (eq nat (S
-i0) O)).(let H3 \def (eq_ind nat (S i0) (\lambda (e: nat).(match e in nat
-return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
-True])) I O H2) in (False_ind (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1))
-(\lambda (e1: C).(drop h (minus O (S i0)) e1 e2))) H3))) | (le_S m H2)
-\Rightarrow (\lambda (H3: (eq nat (S m) O)).((let H4 \def (eq_ind nat (S m)
-(\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O
-\Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind ((le (S
-i0) m) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1:
-C).(drop h (minus O (S i0)) e1 e2)))) H4)) H2))]) in (H2 (refl_equal nat
-O)))))))))) (\lambda (d0: nat).(\lambda (_: (((le (S i0) d0) \to (\forall
+O c1 c2)).(\lambda (e2: C).(\lambda (_: (drop (S i0) O c2 e2)).(ex2_ind nat
+(\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le i0 n)) (ex2 C
+(\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1: C).(drop h (minus O (S
+i0)) e1 e2))) (\lambda (x: nat).(\lambda (H2: (eq nat O (S x))).(\lambda (_:
+(le i0 x)).(let H4 \def (eq_ind nat O (\lambda (ee: nat).(match ee in nat
+return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow
+False])) I (S x) H2) in (False_ind (ex2 C (\lambda (e1: C).(drop (S i0) O c1
+e1)) (\lambda (e1: C).(drop h (minus O (S i0)) e1 e2))) H4))))) (le_gen_S i0
+O H))))))))) (\lambda (d0: nat).(\lambda (_: (((le (S i0) d0) \to (\forall
(c1: C).(\forall (c2: C).(\forall (h: nat).((drop h d0 c1 c2) \to (\forall
(e2: C).((drop (S i0) O c2 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1
e1)) (\lambda (e1: C).(drop h (minus d0 (S i0)) e1 e2)))))))))))).(\lambda
(\lambda (c1: C).(\lambda (c2: C).(\lambda (d: nat).(\lambda (h:
nat).(\lambda (H: (drop h d c1 c2)).(\lambda (e2: C).(\lambda (H0: (drop O O
c2 e2)).(\lambda (H1: (le d O)).(eq_ind C c2 (\lambda (c: C).(drop (plus O h)
-O c1 c)) (let H2 \def (match H1 in le return (\lambda (n: nat).(\lambda (_:
-(le ? n)).((eq nat n O) \to (drop (plus O h) O c1 c2)))) with [le_n
-\Rightarrow (\lambda (H2: (eq nat d O)).(eq_ind nat O (\lambda (_: nat).(drop
-(plus O h) O c1 c2)) (let H3 \def (eq_ind nat d (\lambda (n: nat).(le n O))
-H1 O H2) in (let H4 \def (eq_ind nat d (\lambda (n: nat).(drop h n c1 c2)) H
-O H2) in H4)) d (sym_eq nat d O H2))) | (le_S m H2) \Rightarrow (\lambda (H3:
-(eq nat (S m) O)).((let H4 \def (eq_ind nat (S m) (\lambda (e: nat).(match e
-in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
-\Rightarrow True])) I O H3) in (False_ind ((le d m) \to (drop (plus O h) O c1
-c2)) H4)) H2))]) in (H2 (refl_equal nat O))) e2 (drop_gen_refl c2 e2
+O c1 c)) (let H_y \def (le_n_O_eq d H1) in (let H2 \def (eq_ind_r nat d
+(\lambda (n: nat).(drop h n c1 c2)) H O H_y) in H2)) e2 (drop_gen_refl c2 e2
H0)))))))))) (\lambda (i0: nat).(\lambda (IHi: ((\forall (c1: C).(\forall
(c2: C).(\forall (d: nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall
(e2: C).((drop i0 O c2 e2) \to ((le d i0) \to (drop (plus i0 h) O c1
projects / helm.git / blobdiff