X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fdrop%2Fprops.ma;h=a0744633e65274ecac4bf95e63a5a2bde6f746d4;hb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;hp=95761db5ce20a3f6b6c8fee082f36bf2db91a757;hpb=e92710b1d9774a6491122668c8463b8658114610;p=helm.git diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma index 95761db5c..a0744633e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma @@ -346,115 +346,108 @@ nat).((drop h d c e) \to ((le (plus d h) n) \to (drop (minus n h) O e 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 @@ -538,20 +531,15 @@ C).(\forall (h: nat).((drop h n 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 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 @@ -640,16 +628,8 @@ C).((drop n O c2 e2) \to ((le d n) \to (drop (plus n h) O c1 e2)))))))))) (\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