matita/matita/contribs/lambdadelta/basic_1A/drop/props.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "basic_1A/drop/fwd.ma".
  18
  19 lemma drop_skip_bind:
  20  \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h
  21 d c e) \to (\forall (b: B).(\forall (u: T).(drop h (S d) (CHead c (Bind b)
  22 (lift h d u)) (CHead e (Bind b) u))))))))
  23 \def
  24  \lambda (h: nat).(\lambda (d: nat).(\lambda (c: C).(\lambda (e: C).(\lambda
  25 (H: (drop h d c e)).(\lambda (b: B).(\lambda (u: T).(eq_ind nat (r (Bind b)
  26 d) (\lambda (n: nat).(drop h (S d) (CHead c (Bind b) (lift h n u)) (CHead e
  27 (Bind b) u))) (drop_skip (Bind b) h d c e H u) d (refl_equal nat d)))))))).
  28
  29 lemma drop_skip_flat:
  30  \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h
  31 (S d) c e) \to (\forall (f: F).(\forall (u: T).(drop h (S d) (CHead c (Flat
  32 f) (lift h (S d) u)) (CHead e (Flat f) u))))))))
  33 \def
  34  \lambda (h: nat).(\lambda (d: nat).(\lambda (c: C).(\lambda (e: C).(\lambda
  35 (H: (drop h (S d) c e)).(\lambda (f: F).(\lambda (u: T).(eq_ind nat (r (Flat
  36 f) d) (\lambda (n: nat).(drop h (S d) (CHead c (Flat f) (lift h n u)) (CHead
  37 e (Flat f) u))) (drop_skip (Flat f) h d c e H u) (S d) (refl_equal nat (S
  38 d))))))))).
  39
  40 lemma drop_ctail:
  41  \forall (c1: C).(\forall (c2: C).(\forall (d: nat).(\forall (h: nat).((drop
  42 h d c1 c2) \to (\forall (k: K).(\forall (u: T).(drop h d (CTail k u c1)
  43 (CTail k u c2))))))))
  44 \def
  45  \lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).(\forall (d:
  46 nat).(\forall (h: nat).((drop h d c c2) \to (\forall (k: K).(\forall (u:
  47 T).(drop h d (CTail k u c) (CTail k u c2))))))))) (\lambda (n: nat).(\lambda
  48 (c2: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H: (drop h d (CSort n)
  49 c2)).(\lambda (k: K).(\lambda (u: T).(and3_ind (eq C c2 (CSort n)) (eq nat h
  50 O) (eq nat d O) (drop h d (CTail k u (CSort n)) (CTail k u c2)) (\lambda (H0:
  51 (eq C c2 (CSort n))).(\lambda (H1: (eq nat h O)).(\lambda (H2: (eq nat d
  52 O)).(eq_ind_r nat O (\lambda (n0: nat).(drop n0 d (CTail k u (CSort n))
  53 (CTail k u c2))) (eq_ind_r nat O (\lambda (n0: nat).(drop O n0 (CTail k u
  54 (CSort n)) (CTail k u c2))) (eq_ind_r C (CSort n) (\lambda (c: C).(drop O O
  55 (CTail k u (CSort n)) (CTail k u c))) (drop_refl (CTail k u (CSort n))) c2
  56 H0) d H2) h H1)))) (drop_gen_sort n h d c2 H))))))))) (\lambda (c2:
  57 C).(\lambda (IHc: ((\forall (c3: C).(\forall (d: nat).(\forall (h:
  58 nat).((drop h d c2 c3) \to (\forall (k: K).(\forall (u: T).(drop h d (CTail k
  59 u c2) (CTail k u c3)))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c3:
  60 C).(\lambda (d: nat).(nat_ind (\lambda (n: nat).(\forall (h: nat).((drop h n
  61 (CHead c2 k t) c3) \to (\forall (k0: K).(\forall (u: T).(drop h n (CTail k0 u
  62 (CHead c2 k t)) (CTail k0 u c3))))))) (\lambda (h: nat).(nat_ind (\lambda (n:
  63 nat).((drop n O (CHead c2 k t) c3) \to (\forall (k0: K).(\forall (u: T).(drop
  64 n O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)))))) (\lambda (H: (drop O O
  65 (CHead c2 k t) c3)).(\lambda (k0: K).(\lambda (u: T).(eq_ind C (CHead c2 k t)
  66 (\lambda (c: C).(drop O O (CTail k0 u (CHead c2 k t)) (CTail k0 u c)))
  67 (drop_refl (CTail k0 u (CHead c2 k t))) c3 (drop_gen_refl (CHead c2 k t) c3
  68 H))))) (\lambda (n: nat).(\lambda (_: (((drop n O (CHead c2 k t) c3) \to
  69 (\forall (k0: K).(\forall (u: T).(drop n O (CTail k0 u (CHead c2 k t)) (CTail
  70 k0 u c3))))))).(\lambda (H0: (drop (S n) O (CHead c2 k t) c3)).(\lambda (k0:
  71 K).(\lambda (u: T).(drop_drop k n (CTail k0 u c2) (CTail k0 u c3) (IHc c3 O
  72 (r k n) (drop_gen_drop k c2 c3 t n H0) k0 u) t)))))) h)) (\lambda (n:
  73 nat).(\lambda (H: ((\forall (h: nat).((drop h n (CHead c2 k t) c3) \to
  74 (\forall (k0: K).(\forall (u: T).(drop h n (CTail k0 u (CHead c2 k t)) (CTail
  75 k0 u c3)))))))).(\lambda (h: nat).(\lambda (H0: (drop h (S n) (CHead c2 k t)
  76 c3)).(\lambda (k0: K).(\lambda (u: T).(ex3_2_ind C T (\lambda (e: C).(\lambda
  77 (v: T).(eq C c3 (CHead e k v)))) (\lambda (_: C).(\lambda (v: T).(eq T t
  78 (lift h (r k n) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r k n) c2 e)))
  79 (drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)) (\lambda (x0:
  80 C).(\lambda (x1: T).(\lambda (H1: (eq C c3 (CHead x0 k x1))).(\lambda (H2:
  81 (eq T t (lift h (r k n) x1))).(\lambda (H3: (drop h (r k n) c2 x0)).(let H4
  82 \def (eq_ind C c3 (\lambda (c: C).(\forall (h0: nat).((drop h0 n (CHead c2 k
  83 t) c) \to (\forall (k1: K).(\forall (u0: T).(drop h0 n (CTail k1 u0 (CHead c2
  84 k t)) (CTail k1 u0 c))))))) H (CHead x0 k x1) H1) in (eq_ind_r C (CHead x0 k
  85 x1) (\lambda (c: C).(drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u
  86 c))) (let H5 \def (eq_ind T t (\lambda (t0: T).(\forall (h0: nat).((drop h0 n
  87 (CHead c2 k t0) (CHead x0 k x1)) \to (\forall (k1: K).(\forall (u0: T).(drop
  88 h0 n (CTail k1 u0 (CHead c2 k t0)) (CTail k1 u0 (CHead x0 k x1)))))))) H4
  89 (lift h (r k n) x1) H2) in (eq_ind_r T (lift h (r k n) x1) (\lambda (t0:
  90 T).(drop h (S n) (CTail k0 u (CHead c2 k t0)) (CTail k0 u (CHead x0 k x1))))
  91 (drop_skip k h n (CTail k0 u c2) (CTail k0 u x0) (IHc x0 (r k n) h H3 k0 u)
  92 x1) t H2)) c3 H1))))))) (drop_gen_skip_l c2 c3 t h n k H0)))))))) d)))))))
  93 c1).
  94
  95 theorem drop_conf_lt:
  96  \forall (k: K).(\forall (i: nat).(\forall (u: T).(\forall (c0: C).(\forall
  97 (c: C).((drop i O c (CHead c0 k u)) \to (\forall (e: C).(\forall (h:
  98 nat).(\forall (d: nat).((drop h (S (plus i d)) c e) \to (ex3_2 T C (\lambda
  99 (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 100 (e0: C).(drop i O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop
 101 h (r k d) c0 e0)))))))))))))
 102 \def
 103  \lambda (k: K).(\lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (u:
 104 T).(\forall (c0: C).(\forall (c: C).((drop n O c (CHead c0 k u)) \to (\forall
 105 (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus n d)) c e) \to
 106 (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v))))
 107 (\lambda (v: T).(\lambda (e0: C).(drop n O e (CHead e0 k v)))) (\lambda (_:
 108 T).(\lambda (e0: C).(drop h (r k d) c0 e0))))))))))))) (\lambda (u:
 109 T).(\lambda (c0: C).(\lambda (c: C).(\lambda (H: (drop O O c (CHead c0 k
 110 u))).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H0: (drop
 111 h (S (plus O d)) c e)).(let H1 \def (eq_ind C c (\lambda (c1: C).(drop h (S
 112 (plus O d)) c1 e)) H0 (CHead c0 k u) (drop_gen_refl c (CHead c0 k u) H)) in
 113 (ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 k v))))
 114 (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k (plus O d)) v))))
 115 (\lambda (e0: C).(\lambda (_: T).(drop h (r k (plus O d)) c0 e0))) (ex3_2 T C
 116 (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v:
 117 T).(\lambda (e0: C).(drop O O e (CHead e0 k v)))) (\lambda (_: T).(\lambda
 118 (e0: C).(drop h (r k d) c0 e0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda
 119 (H2: (eq C e (CHead x0 k x1))).(\lambda (H3: (eq T u (lift h (r k (plus O d))
 120 x1))).(\lambda (H4: (drop h (r k (plus O d)) c0 x0)).(eq_ind_r C (CHead x0 k
 121 x1) (\lambda (c1: C).(ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift
 122 h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop O O c1 (CHead e0 k
 123 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))) (eq_ind_r T
 124 (lift h (r k (plus O d)) x1) (\lambda (t: T).(ex3_2 T C (\lambda (v:
 125 T).(\lambda (_: C).(eq T t (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 126 (e0: C).(drop O O (CHead x0 k x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda
 127 (e0: C).(drop h (r k d) c0 e0))))) (ex3_2_intro T C (\lambda (v: T).(\lambda
 128 (_: C).(eq T (lift h (r k (plus O d)) x1) (lift h (r k d) v)))) (\lambda (v:
 129 T).(\lambda (e0: C).(drop O O (CHead x0 k x1) (CHead e0 k v)))) (\lambda (_:
 130 T).(\lambda (e0: C).(drop h (r k d) c0 e0))) x1 x0 (refl_equal T (lift h (r k
 131 d) x1)) (drop_refl (CHead x0 k x1)) H4) u H3) e H2)))))) (drop_gen_skip_l c0
 132 e u h (plus O d) k H1))))))))))) (\lambda (i0: nat).(\lambda (H: ((\forall
 133 (u: T).(\forall (c0: C).(\forall (c: C).((drop i0 O c (CHead c0 k u)) \to
 134 (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus i0 d))
 135 c e) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d)
 136 v)))) (\lambda (v: T).(\lambda (e0: C).(drop i0 O e (CHead e0 k v))))
 137 (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))))))))))))).(\lambda
 138 (u: T).(\lambda (c0: C).(\lambda (c: C).(C_ind (\lambda (c1: C).((drop (S i0)
 139 O c1 (CHead c0 k u)) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
 140 nat).((drop h (S (plus (S i0) d)) c1 e) \to (ex3_2 T C (\lambda (v:
 141 T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 142 (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
 143 C).(drop h (r k d) c0 e0)))))))))) (\lambda (n: nat).(\lambda (_: (drop (S
 144 i0) O (CSort n) (CHead c0 k u))).(\lambda (e: C).(\lambda (h: nat).(\lambda
 145 (d: nat).(\lambda (H1: (drop h (S (plus (S i0) d)) (CSort n) e)).(and3_ind
 146 (eq C e (CSort n)) (eq nat h O) (eq nat (S (plus (S i0) d)) O) (ex3_2 T C
 147 (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v:
 148 T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_:
 149 T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) (\lambda (_: (eq C e (CSort
 150 n))).(\lambda (_: (eq nat h O)).(\lambda (H4: (eq nat (S (plus (S i0) d))
 151 O)).(let H5 \def (eq_ind nat (S (plus (S i0) d)) (\lambda (ee: nat).(match ee
 152 with [O \Rightarrow False | (S _) \Rightarrow True])) I O H4) in (False_ind
 153 (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v))))
 154 (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda
 155 (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) H5))))) (drop_gen_sort n h
 156 (S (plus (S i0) d)) e H1)))))))) (\lambda (c1: C).(\lambda (H0: (((drop (S
 157 i0) O c1 (CHead c0 k u)) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
 158 nat).((drop h (S (plus (S i0) d)) c1 e) \to (ex3_2 T C (\lambda (v:
 159 T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 160 (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
 161 C).(drop h (r k d) c0 e0))))))))))).(\lambda (k0: K).(K_ind (\lambda (k1:
 162 K).(\forall (t: T).((drop (S i0) O (CHead c1 k1 t) (CHead c0 k u)) \to
 163 (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus (S i0)
 164 d)) (CHead c1 k1 t) e) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u
 165 (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O e
 166 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0
 167 e0))))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (H1: (drop (S i0) O
 168 (CHead c1 (Bind b) t) (CHead c0 k u))).(\lambda (e: C).(\lambda (h:
 169 nat).(\lambda (d: nat).(\lambda (H2: (drop h (S (plus (S i0) d)) (CHead c1
 170 (Bind b) t) e)).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e
 171 (CHead e0 (Bind b) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r
 172 (Bind b) (plus (S i0) d)) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r
 173 (Bind b) (plus (S i0) d)) c1 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_:
 174 C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S
 175 i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0
 176 e0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H3: (eq C e (CHead x0
 177 (Bind b) x1))).(\lambda (_: (eq T t (lift h (r (Bind b) (plus (S i0) d))
 178 x1))).(\lambda (H5: (drop h (r (Bind b) (plus (S i0) d)) c1 x0)).(eq_ind_r C
 179 (CHead x0 (Bind b) x1) (\lambda (c2: C).(ex3_2 T C (\lambda (v: T).(\lambda
 180 (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop
 181 (S i0) O c2 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k
 182 d) c0 e0))))) (let H6 \def (H u c0 c1 (drop_gen_drop (Bind b) c1 (CHead c0 k
 183 u) t i0 H1) x0 h d H5) in (ex3_2_ind T C (\lambda (v: T).(\lambda (_: C).(eq
 184 T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop i0 O x0
 185 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))
 186 (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v))))
 187 (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Bind b) x1) (CHead
 188 e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))
 189 (\lambda (x2: T).(\lambda (x3: C).(\lambda (H7: (eq T u (lift h (r k d)
 190 x2))).(\lambda (H8: (drop i0 O x0 (CHead x3 k x2))).(\lambda (H9: (drop h (r
 191 k d) c0 x3)).(ex3_2_intro T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h
 192 (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Bind
 193 b) x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0
 194 e0))) x2 x3 H7 (drop_drop (Bind b) i0 x0 (CHead x3 k x2) H8 x1) H9)))))) H6))
 195 e H3)))))) (drop_gen_skip_l c1 e t h (plus (S i0) d) (Bind b) H2)))))))))
 196 (\lambda (f: F).(\lambda (t: T).(\lambda (H1: (drop (S i0) O (CHead c1 (Flat
 197 f) t) (CHead c0 k u))).(\lambda (e: C).(\lambda (h: nat).(\lambda (d:
 198 nat).(\lambda (H2: (drop h (S (plus (S i0) d)) (CHead c1 (Flat f) t)
 199 e)).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 (Flat
 200 f) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r (Flat f) (plus (S
 201 i0) d)) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r (Flat f) (plus (S
 202 i0) d)) c1 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h
 203 (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k
 204 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) (\lambda
 205 (x0: C).(\lambda (x1: T).(\lambda (H3: (eq C e (CHead x0 (Flat f)
 206 x1))).(\lambda (_: (eq T t (lift h (r (Flat f) (plus (S i0) d))
 207 x1))).(\lambda (H5: (drop h (r (Flat f) (plus (S i0) d)) c1 x0)).(eq_ind_r C
 208 (CHead x0 (Flat f) x1) (\lambda (c2: C).(ex3_2 T C (\lambda (v: T).(\lambda
 209 (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop
 210 (S i0) O c2 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k
 211 d) c0 e0))))) (ex3_2_ind T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h
 212 (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O x0 (CHead e0 k
 213 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))) (ex3_2 T C
 214 (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v:
 215 T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Flat f) x1) (CHead e0 k v))))
 216 (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) (\lambda (x2:
 217 T).(\lambda (x3: C).(\lambda (H6: (eq T u (lift h (r k d) x2))).(\lambda (H7:
 218 (drop (S i0) O x0 (CHead x3 k x2))).(\lambda (H8: (drop h (r k d) c0
 219 x3)).(ex3_2_intro T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d)
 220 v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Flat f) x1)
 221 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))
 222 x2 x3 H6 (drop_drop (Flat f) i0 x0 (CHead x3 k x2) H7 x1) H8)))))) (H0
 223 (drop_gen_drop (Flat f) c1 (CHead c0 k u) t i0 H1) x0 h d H5)) e H3))))))
 224 (drop_gen_skip_l c1 e t h (plus (S i0) d) (Flat f) H2))))))))) k0)))) c))))))
 225 i)).
 226
 227 theorem drop_conf_ge:
 228  \forall (i: nat).(\forall (a: C).(\forall (c: C).((drop i O c a) \to
 229 (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c e) \to ((le
 230 (plus d h) i) \to (drop (minus i h) O e a)))))))))
 231 \def
 232  \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (a: C).(\forall (c:
 233 C).((drop n O c a) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
 234 nat).((drop h d c e) \to ((le (plus d h) n) \to (drop (minus n h) O e
 235 a)))))))))) (\lambda (a: C).(\lambda (c: C).(\lambda (H: (drop O O c
 236 a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H0: (drop h
 237 d c e)).(\lambda (H1: (le (plus d h) O)).(let H2 \def (eq_ind C c (\lambda
 238 (c0: C).(drop h d c0 e)) H0 a (drop_gen_refl c a H)) in (let H_y \def
 239 (le_n_O_eq (plus d h) H1) in (land_ind (eq nat d O) (eq nat h O) (drop (minus
 240 O h) O e a) (\lambda (H3: (eq nat d O)).(\lambda (H4: (eq nat h O)).(let H5
 241 \def (eq_ind nat d (\lambda (n: nat).(drop h n a e)) H2 O H3) in (let H6 \def
 242 (eq_ind nat h (\lambda (n: nat).(drop n O a e)) H5 O H4) in (eq_ind_r nat O
 243 (\lambda (n: nat).(drop (minus O n) O e a)) (eq_ind C a (\lambda (c0:
 244 C).(drop (minus O O) O c0 a)) (drop_refl a) e (drop_gen_refl a e H6)) h
 245 H4))))) (plus_O d h (sym_eq nat O (plus d h) H_y))))))))))))) (\lambda (i0:
 246 nat).(\lambda (H: ((\forall (a: C).(\forall (c: C).((drop i0 O c a) \to
 247 (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c e) \to ((le
 248 (plus d h) i0) \to (drop (minus i0 h) O e a))))))))))).(\lambda (a:
 249 C).(\lambda (c: C).(C_ind (\lambda (c0: C).((drop (S i0) O c0 a) \to (\forall
 250 (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c0 e) \to ((le (plus d
 251 h) (S i0)) \to (drop (minus (S i0) h) O e a)))))))) (\lambda (n:
 252 nat).(\lambda (H0: (drop (S i0) O (CSort n) a)).(\lambda (e: C).(\lambda (h:
 253 nat).(\lambda (d: nat).(\lambda (H1: (drop h d (CSort n) e)).(\lambda (H2:
 254 (le (plus d h) (S i0))).(and3_ind (eq C e (CSort n)) (eq nat h O) (eq nat d
 255 O) (drop (minus (S i0) h) O e a) (\lambda (H3: (eq C e (CSort n))).(\lambda
 256 (H4: (eq nat h O)).(\lambda (H5: (eq nat d O)).(and3_ind (eq C a (CSort n))
 257 (eq nat (S i0) O) (eq nat O O) (drop (minus (S i0) h) O e a) (\lambda (H6:
 258 (eq C a (CSort n))).(\lambda (H7: (eq nat (S i0) O)).(\lambda (_: (eq nat O
 259 O)).(let H9 \def (eq_ind nat d (\lambda (n0: nat).(le (plus n0 h) (S i0))) H2
 260 O H5) in (let H10 \def (eq_ind nat h (\lambda (n0: nat).(le (plus O n0) (S
 261 i0))) H9 O H4) in (eq_ind_r nat O (\lambda (n0: nat).(drop (minus (S i0) n0)
 262 O e a)) (eq_ind_r C (CSort n) (\lambda (c0: C).(drop (minus (S i0) O) O c0
 263 a)) (eq_ind_r C (CSort n) (\lambda (c0: C).(drop (minus (S i0) O) O (CSort n)
 264 c0)) (let H11 \def (eq_ind nat (S i0) (\lambda (ee: nat).(match ee with [O
 265 \Rightarrow False | (S _) \Rightarrow True])) I O H7) in (False_ind (drop
 266 (minus (S i0) O) O (CSort n) (CSort n)) H11)) a H6) e H3) h H4))))))
 267 (drop_gen_sort n (S i0) O a H0))))) (drop_gen_sort n h d e H1)))))))))
 268 (\lambda (c0: C).(\lambda (H0: (((drop (S i0) O c0 a) \to (\forall (e:
 269 C).(\forall (h: nat).(\forall (d: nat).((drop h d c0 e) \to ((le (plus d h)
 270 (S i0)) \to (drop (minus (S i0) h) O e a))))))))).(\lambda (k: K).(K_ind
 271 (\lambda (k0: K).(\forall (t: T).((drop (S i0) O (CHead c0 k0 t) a) \to
 272 (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d (CHead c0 k0
 273 t) e) \to ((le (plus d h) (S i0)) \to (drop (minus (S i0) h) O e a)))))))))
 274 (\lambda (b: B).(\lambda (t: T).(\lambda (H1: (drop (S i0) O (CHead c0 (Bind
 275 b) t) a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H2:
 276 (drop h d (CHead c0 (Bind b) t) e)).(\lambda (H3: (le (plus d h) (S
 277 i0))).(nat_ind (\lambda (n: nat).((drop h n (CHead c0 (Bind b) t) e) \to ((le
 278 (plus n h) (S i0)) \to (drop (minus (S i0) h) O e a)))) (\lambda (H4: (drop h
 279 O (CHead c0 (Bind b) t) e)).(\lambda (H5: (le (plus O h) (S i0))).(nat_ind
 280 (\lambda (n: nat).((drop n O (CHead c0 (Bind b) t) e) \to ((le (plus O n) (S
 281 i0)) \to (drop (minus (S i0) n) O e a)))) (\lambda (H6: (drop O O (CHead c0
 282 (Bind b) t) e)).(\lambda (_: (le (plus O O) (S i0))).(eq_ind C (CHead c0
 283 (Bind b) t) (\lambda (c1: C).(drop (minus (S i0) O) O c1 a)) (drop_drop (Bind
 284 b) i0 c0 a (drop_gen_drop (Bind b) c0 a t i0 H1) t) e (drop_gen_refl (CHead
 285 c0 (Bind b) t) e H6)))) (\lambda (h0: nat).(\lambda (_: (((drop h0 O (CHead
 286 c0 (Bind b) t) e) \to ((le (plus O h0) (S i0)) \to (drop (minus (S i0) h0) O
 287 e a))))).(\lambda (H6: (drop (S h0) O (CHead c0 (Bind b) t) e)).(\lambda (H7:
 288 (le (plus O (S h0)) (S i0))).(H a c0 (drop_gen_drop (Bind b) c0 a t i0 H1) e
 289 h0 O (drop_gen_drop (Bind b) c0 e t h0 H6) (le_S_n (plus O h0) i0 H7)))))) h
 290 H4 H5))) (\lambda (d0: nat).(\lambda (_: (((drop h d0 (CHead c0 (Bind b) t)
 291 e) \to ((le (plus d0 h) (S i0)) \to (drop (minus (S i0) h) O e
 292 a))))).(\lambda (H4: (drop h (S d0) (CHead c0 (Bind b) t) e)).(\lambda (H5:
 293 (le (plus (S d0) h) (S i0))).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v:
 294 T).(eq C e (CHead e0 (Bind b) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t
 295 (lift h (r (Bind b) d0) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r
 296 (Bind b) d0) c0 e0))) (drop (minus (S i0) h) O e a) (\lambda (x0: C).(\lambda
 297 (x1: T).(\lambda (H6: (eq C e (CHead x0 (Bind b) x1))).(\lambda (_: (eq T t
 298 (lift h (r (Bind b) d0) x1))).(\lambda (H8: (drop h (r (Bind b) d0) c0
 299 x0)).(eq_ind_r C (CHead x0 (Bind b) x1) (\lambda (c1: C).(drop (minus (S i0)
 300 h) O c1 a)) (eq_ind nat (S (minus i0 h)) (\lambda (n: nat).(drop n O (CHead
 301 x0 (Bind b) x1) a)) (drop_drop (Bind b) (minus i0 h) x0 a (H a c0
 302 (drop_gen_drop (Bind b) c0 a t i0 H1) x0 h d0 H8 (le_S_n (plus d0 h) i0 H5))
 303 x1) (minus (S i0) h) (minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus
 304 d0 h) i0 H5)))) e H6)))))) (drop_gen_skip_l c0 e t h d0 (Bind b) H4)))))) d
 305 H2 H3))))))))) (\lambda (f: F).(\lambda (t: T).(\lambda (H1: (drop (S i0) O
 306 (CHead c0 (Flat f) t) a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d:
 307 nat).(\lambda (H2: (drop h d (CHead c0 (Flat f) t) e)).(\lambda (H3: (le
 308 (plus d h) (S i0))).(nat_ind (\lambda (n: nat).((drop h n (CHead c0 (Flat f)
 309 t) e) \to ((le (plus n h) (S i0)) \to (drop (minus (S i0) h) O e a))))
 310 (\lambda (H4: (drop h O (CHead c0 (Flat f) t) e)).(\lambda (H5: (le (plus O
 311 h) (S i0))).(nat_ind (\lambda (n: nat).((drop n O (CHead c0 (Flat f) t) e)
 312 \to ((le (plus O n) (S i0)) \to (drop (minus (S i0) n) O e a)))) (\lambda
 313 (H6: (drop O O (CHead c0 (Flat f) t) e)).(\lambda (_: (le (plus O O) (S
 314 i0))).(eq_ind C (CHead c0 (Flat f) t) (\lambda (c1: C).(drop (minus (S i0) O)
 315 O c1 a)) (drop_drop (Flat f) i0 c0 a (drop_gen_drop (Flat f) c0 a t i0 H1) t)
 316 e (drop_gen_refl (CHead c0 (Flat f) t) e H6)))) (\lambda (h0: nat).(\lambda
 317 (_: (((drop h0 O (CHead c0 (Flat f) t) e) \to ((le (plus O h0) (S i0)) \to
 318 (drop (minus (S i0) h0) O e a))))).(\lambda (H6: (drop (S h0) O (CHead c0
 319 (Flat f) t) e)).(\lambda (H7: (le (plus O (S h0)) (S i0))).(H0 (drop_gen_drop
 320 (Flat f) c0 a t i0 H1) e (S h0) O (drop_gen_drop (Flat f) c0 e t h0 H6)
 321 H7))))) h H4 H5))) (\lambda (d0: nat).(\lambda (_: (((drop h d0 (CHead c0
 322 (Flat f) t) e) \to ((le (plus d0 h) (S i0)) \to (drop (minus (S i0) h) O e
 323 a))))).(\lambda (H4: (drop h (S d0) (CHead c0 (Flat f) t) e)).(\lambda (H5:
 324 (le (plus (S d0) h) (S i0))).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v:
 325 T).(eq C e (CHead e0 (Flat f) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t
 326 (lift h (r (Flat f) d0) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r
 327 (Flat f) d0) c0 e0))) (drop (minus (S i0) h) O e a) (\lambda (x0: C).(\lambda
 328 (x1: T).(\lambda (H6: (eq C e (CHead x0 (Flat f) x1))).(\lambda (_: (eq T t
 329 (lift h (r (Flat f) d0) x1))).(\lambda (H8: (drop h (r (Flat f) d0) c0
 330 x0)).(eq_ind_r C (CHead x0 (Flat f) x1) (\lambda (c1: C).(drop (minus (S i0)
 331 h) O c1 a)) (let H9 \def (eq_ind_r nat (minus (S i0) h) (\lambda (n:
 332 nat).(drop n O x0 a)) (H0 (drop_gen_drop (Flat f) c0 a t i0 H1) x0 h (S d0)
 333 H8 H5) (S (minus i0 h)) (minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n
 334 (plus d0 h) i0 H5)))) in (eq_ind nat (S (minus i0 h)) (\lambda (n: nat).(drop
 335 n O (CHead x0 (Flat f) x1) a)) (drop_drop (Flat f) (minus i0 h) x0 a H9 x1)
 336 (minus (S i0) h) (minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0
 337 h) i0 H5))))) e H6)))))) (drop_gen_skip_l c0 e t h d0 (Flat f) H4)))))) d H2
 338 H3))))))))) k)))) c))))) i).
 339
 340 theorem drop_conf_rev:
 341  \forall (j: nat).(\forall (e1: C).(\forall (e2: C).((drop j O e1 e2) \to
 342 (\forall (c2: C).(\forall (i: nat).((drop i O c2 e2) \to (ex2 C (\lambda (c1:
 343 C).(drop j O c1 c2)) (\lambda (c1: C).(drop i j c1 e1)))))))))
 344 \def
 345  \lambda (j: nat).(nat_ind (\lambda (n: nat).(\forall (e1: C).(\forall (e2:
 346 C).((drop n O e1 e2) \to (\forall (c2: C).(\forall (i: nat).((drop i O c2 e2)
 347 \to (ex2 C (\lambda (c1: C).(drop n O c1 c2)) (\lambda (c1: C).(drop i n c1
 348 e1)))))))))) (\lambda (e1: C).(\lambda (e2: C).(\lambda (H: (drop O O e1
 349 e2)).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H0: (drop i O c2 e2)).(let
 350 H1 \def (eq_ind_r C e2 (\lambda (c: C).(drop i O c2 c)) H0 e1 (drop_gen_refl
 351 e1 e2 H)) in (ex_intro2 C (\lambda (c1: C).(drop O O c1 c2)) (\lambda (c1:
 352 C).(drop i O c1 e1)) c2 (drop_refl c2) H1)))))))) (\lambda (j0: nat).(\lambda
 353 (IHj: ((\forall (e1: C).(\forall (e2: C).((drop j0 O e1 e2) \to (\forall (c2:
 354 C).(\forall (i: nat).((drop i O c2 e2) \to (ex2 C (\lambda (c1: C).(drop j0 O
 355 c1 c2)) (\lambda (c1: C).(drop i j0 c1 e1))))))))))).(\lambda (e1: C).(C_ind
 356 (\lambda (c: C).(\forall (e2: C).((drop (S j0) O c e2) \to (\forall (c2:
 357 C).(\forall (i: nat).((drop i O c2 e2) \to (ex2 C (\lambda (c1: C).(drop (S
 358 j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 c))))))))) (\lambda (n:
 359 nat).(\lambda (e2: C).(\lambda (H: (drop (S j0) O (CSort n) e2)).(\lambda
 360 (c2: C).(\lambda (i: nat).(\lambda (H0: (drop i O c2 e2)).(and3_ind (eq C e2
 361 (CSort n)) (eq nat (S j0) O) (eq nat O O) (ex2 C (\lambda (c1: C).(drop (S
 362 j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CSort n)))) (\lambda (H1:
 363 (eq C e2 (CSort n))).(\lambda (H2: (eq nat (S j0) O)).(\lambda (_: (eq nat O
 364 O)).(let H4 \def (eq_ind C e2 (\lambda (c: C).(drop i O c2 c)) H0 (CSort n)
 365 H1) in (let H5 \def (eq_ind nat (S j0) (\lambda (ee: nat).(match ee with [O
 366 \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind (ex2 C
 367 (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1
 368 (CSort n)))) H5)))))) (drop_gen_sort n (S j0) O e2 H)))))))) (\lambda (e2:
 369 C).(\lambda (IHe1: ((\forall (e3: C).((drop (S j0) O e2 e3) \to (\forall (c2:
 370 C).(\forall (i: nat).((drop i O c2 e3) \to (ex2 C (\lambda (c1: C).(drop (S
 371 j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 e2)))))))))).(\lambda (k:
 372 K).(\lambda (t: T).(\lambda (e3: C).(\lambda (H: (drop (S j0) O (CHead e2 k
 373 t) e3)).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H0: (drop i O c2
 374 e3)).(K_ind (\lambda (k0: K).((drop (r k0 j0) O e2 e3) \to (ex2 C (\lambda
 375 (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2
 376 k0 t)))))) (\lambda (b: B).(\lambda (H1: (drop (r (Bind b) j0) O e2 e3)).(let
 377 H_x \def (IHj e2 e3 H1 c2 i H0) in (let H2 \def H_x in (ex2_ind C (\lambda
 378 (c1: C).(drop j0 O c1 c2)) (\lambda (c1: C).(drop i j0 c1 e2)) (ex2 C
 379 (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1
 380 (CHead e2 (Bind b) t)))) (\lambda (x: C).(\lambda (H3: (drop j0 O x
 381 c2)).(\lambda (H4: (drop i j0 x e2)).(ex_intro2 C (\lambda (c1: C).(drop (S
 382 j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2 (Bind b) t)))
 383 (CHead x (Bind b) (lift i (r (Bind b) j0) t)) (drop_drop (Bind b) j0 x c2 H3
 384 (lift i (r (Bind b) j0) t)) (drop_skip (Bind b) i j0 x e2 H4 t))))) H2)))))
 385 (\lambda (f: F).(\lambda (H1: (drop (r (Flat f) j0) O e2 e3)).(let H_x \def
 386 (IHe1 e3 H1 c2 i H0) in (let H2 \def H_x in (ex2_ind C (\lambda (c1: C).(drop
 387 (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 e2)) (ex2 C (\lambda (c1:
 388 C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2 (Flat
 389 f) t)))) (\lambda (x: C).(\lambda (H3: (drop (S j0) O x c2)).(\lambda (H4:
 390 (drop i (S j0) x e2)).(ex_intro2 C (\lambda (c1: C).(drop (S j0) O c1 c2))
 391 (\lambda (c1: C).(drop i (S j0) c1 (CHead e2 (Flat f) t))) (CHead x (Flat f)
 392 (lift i (r (Flat f) j0) t)) (drop_drop (Flat f) j0 x c2 H3 (lift i (r (Flat
 393 f) j0) t)) (drop_skip (Flat f) i j0 x e2 H4 t))))) H2))))) k (drop_gen_drop k
 394 e2 e3 t j0 H))))))))))) e1)))) j).
 395
 396 theorem drop_trans_le:
 397  \forall (i: nat).(\forall (d: nat).((le i d) \to (\forall (c1: C).(\forall
 398 (c2: C).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((drop i O
 399 c2 e2) \to (ex2 C (\lambda (e1: C).(drop i O c1 e1)) (\lambda (e1: C).(drop h
 400 (minus d i) e1 e2)))))))))))
 401 \def
 402  \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (d: nat).((le n d) \to
 403 (\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((drop h d c1 c2) \to
 404 (\forall (e2: C).((drop n O c2 e2) \to (ex2 C (\lambda (e1: C).(drop n O c1
 405 e1)) (\lambda (e1: C).(drop h (minus d n) e1 e2)))))))))))) (\lambda (d:
 406 nat).(\lambda (_: (le O d)).(\lambda (c1: C).(\lambda (c2: C).(\lambda (h:
 407 nat).(\lambda (H0: (drop h d c1 c2)).(\lambda (e2: C).(\lambda (H1: (drop O O
 408 c2 e2)).(let H2 \def (eq_ind C c2 (\lambda (c: C).(drop h d c1 c)) H0 e2
 409 (drop_gen_refl c2 e2 H1)) in (eq_ind nat d (\lambda (n: nat).(ex2 C (\lambda
 410 (e1: C).(drop O O c1 e1)) (\lambda (e1: C).(drop h n e1 e2)))) (ex_intro2 C
 411 (\lambda (e1: C).(drop O O c1 e1)) (\lambda (e1: C).(drop h d e1 e2)) c1
 412 (drop_refl c1) H2) (minus d O) (minus_n_O d))))))))))) (\lambda (i0:
 413 nat).(\lambda (IHi: ((\forall (d: nat).((le i0 d) \to (\forall (c1:
 414 C).(\forall (c2: C).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2:
 415 C).((drop i0 O c2 e2) \to (ex2 C (\lambda (e1: C).(drop i0 O c1 e1)) (\lambda
 416 (e1: C).(drop h (minus d i0) e1 e2))))))))))))).(\lambda (d: nat).(nat_ind
 417 (\lambda (n: nat).((le (S i0) n) \to (\forall (c1: C).(\forall (c2:
 418 C).(\forall (h: nat).((drop h n c1 c2) \to (\forall (e2: C).((drop (S i0) O
 419 c2 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1:
 420 C).(drop h (minus n (S i0)) e1 e2))))))))))) (\lambda (H: (le (S i0)
 421 O)).(\lambda (c1: C).(\lambda (c2: C).(\lambda (h: nat).(\lambda (_: (drop h
 422 O c1 c2)).(\lambda (e2: C).(\lambda (_: (drop (S i0) O c2 e2)).(ex2_ind nat
 423 (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le i0 n)) (ex2 C
 424 (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1: C).(drop h (minus O (S
 425 i0)) e1 e2))) (\lambda (x: nat).(\lambda (H2: (eq nat O (S x))).(\lambda (_:
 426 (le i0 x)).(let H4 \def (eq_ind nat O (\lambda (ee: nat).(match ee with [O
 427 \Rightarrow True | (S _) \Rightarrow False])) I (S x) H2) in (False_ind (ex2
 428 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1: C).(drop h (minus O
 429 (S i0)) e1 e2))) H4))))) (le_gen_S i0 O H))))))))) (\lambda (d0:
 430 nat).(\lambda (_: (((le (S i0) d0) \to (\forall (c1: C).(\forall (c2:
 431 C).(\forall (h: nat).((drop h d0 c1 c2) \to (\forall (e2: C).((drop (S i0) O
 432 c2 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1:
 433 C).(drop h (minus d0 (S i0)) e1 e2)))))))))))).(\lambda (H: (le (S i0) (S
 434 d0))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).(\forall (h:
 435 nat).((drop h (S d0) c c2) \to (\forall (e2: C).((drop (S i0) O c2 e2) \to
 436 (ex2 C (\lambda (e1: C).(drop (S i0) O c e1)) (\lambda (e1: C).(drop h (minus
 437 (S d0) (S i0)) e1 e2))))))))) (\lambda (n: nat).(\lambda (c2: C).(\lambda (h:
 438 nat).(\lambda (H0: (drop h (S d0) (CSort n) c2)).(\lambda (e2: C).(\lambda
 439 (H1: (drop (S i0) O c2 e2)).(and3_ind (eq C c2 (CSort n)) (eq nat h O) (eq
 440 nat (S d0) O) (ex2 C (\lambda (e1: C).(drop (S i0) O (CSort n) e1)) (\lambda
 441 (e1: C).(drop h (minus (S d0) (S i0)) e1 e2))) (\lambda (H2: (eq C c2 (CSort
 442 n))).(\lambda (_: (eq nat h O)).(\lambda (_: (eq nat (S d0) O)).(let H5 \def
 443 (eq_ind C c2 (\lambda (c: C).(drop (S i0) O c e2)) H1 (CSort n) H2) in
 444 (and3_ind (eq C e2 (CSort n)) (eq nat (S i0) O) (eq nat O O) (ex2 C (\lambda
 445 (e1: C).(drop (S i0) O (CSort n) e1)) (\lambda (e1: C).(drop h (minus (S d0)
 446 (S i0)) e1 e2))) (\lambda (H6: (eq C e2 (CSort n))).(\lambda (H7: (eq nat (S
 447 i0) O)).(\lambda (_: (eq nat O O)).(eq_ind_r C (CSort n) (\lambda (c: C).(ex2
 448 C (\lambda (e1: C).(drop (S i0) O (CSort n) e1)) (\lambda (e1: C).(drop h
 449 (minus (S d0) (S i0)) e1 c)))) (let H9 \def (eq_ind nat (S i0) (\lambda (ee:
 450 nat).(match ee with [O \Rightarrow False | (S _) \Rightarrow True])) I O H7)
 451 in (False_ind (ex2 C (\lambda (e1: C).(drop (S i0) O (CSort n) e1)) (\lambda
 452 (e1: C).(drop h (minus (S d0) (S i0)) e1 (CSort n)))) H9)) e2 H6))))
 453 (drop_gen_sort n (S i0) O e2 H5)))))) (drop_gen_sort n h (S d0) c2 H0))))))))
 454 (\lambda (c2: C).(\lambda (IHc: ((\forall (c3: C).(\forall (h: nat).((drop h
 455 (S d0) c2 c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to (ex2 C (\lambda
 456 (e1: C).(drop (S i0) O c2 e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0))
 457 e1 e2)))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t:
 458 T).(\forall (c3: C).(\forall (h: nat).((drop h (S d0) (CHead c2 k0 t) c3) \to
 459 (\forall (e2: C).((drop (S i0) O c3 e2) \to (ex2 C (\lambda (e1: C).(drop (S
 460 i0) O (CHead c2 k0 t) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1
 461 e2)))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (c3: C).(\lambda (h:
 462 nat).(\lambda (H0: (drop h (S d0) (CHead c2 (Bind b) t) c3)).(\lambda (e2:
 463 C).(\lambda (H1: (drop (S i0) O c3 e2)).(ex3_2_ind C T (\lambda (e:
 464 C).(\lambda (v: T).(eq C c3 (CHead e (Bind b) v)))) (\lambda (_: C).(\lambda
 465 (v: T).(eq T t (lift h (r (Bind b) d0) v)))) (\lambda (e: C).(\lambda (_:
 466 T).(drop h (r (Bind b) d0) c2 e))) (ex2 C (\lambda (e1: C).(drop (S i0) O
 467 (CHead c2 (Bind b) t) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1
 468 e2))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H2: (eq C c3 (CHead x0
 469 (Bind b) x1))).(\lambda (H3: (eq T t (lift h (r (Bind b) d0) x1))).(\lambda
 470 (H4: (drop h (r (Bind b) d0) c2 x0)).(let H5 \def (eq_ind C c3 (\lambda (c:
 471 C).(drop (S i0) O c e2)) H1 (CHead x0 (Bind b) x1) H2) in (eq_ind_r T (lift h
 472 (r (Bind b) d0) x1) (\lambda (t0: T).(ex2 C (\lambda (e1: C).(drop (S i0) O
 473 (CHead c2 (Bind b) t0) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1
 474 e2)))) (ex2_ind C (\lambda (e1: C).(drop i0 O c2 e1)) (\lambda (e1: C).(drop
 475 h (minus d0 i0) e1 e2)) (ex2 C (\lambda (e1: C).(drop (S i0) O (CHead c2
 476 (Bind b) (lift h (r (Bind b) d0) x1)) e1)) (\lambda (e1: C).(drop h (minus (S
 477 d0) (S i0)) e1 e2))) (\lambda (x: C).(\lambda (H6: (drop i0 O c2 x)).(\lambda
 478 (H7: (drop h (minus d0 i0) x e2)).(ex_intro2 C (\lambda (e1: C).(drop (S i0)
 479 O (CHead c2 (Bind b) (lift h (r (Bind b) d0) x1)) e1)) (\lambda (e1: C).(drop
 480 h (minus (S d0) (S i0)) e1 e2)) x (drop_drop (Bind b) i0 c2 x H6 (lift h (r
 481 (Bind b) d0) x1)) H7)))) (IHi d0 (le_S_n i0 d0 H) c2 x0 h H4 e2
 482 (drop_gen_drop (Bind b) x0 e2 x1 i0 H5))) t H3))))))) (drop_gen_skip_l c2 c3
 483 t h d0 (Bind b) H0))))))))) (\lambda (f: F).(\lambda (t: T).(\lambda (c3:
 484 C).(\lambda (h: nat).(\lambda (H0: (drop h (S d0) (CHead c2 (Flat f) t)
 485 c3)).(\lambda (e2: C).(\lambda (H1: (drop (S i0) O c3 e2)).(ex3_2_ind C T
 486 (\lambda (e: C).(\lambda (v: T).(eq C c3 (CHead e (Flat f) v)))) (\lambda (_:
 487 C).(\lambda (v: T).(eq T t (lift h (r (Flat f) d0) v)))) (\lambda (e:
 488 C).(\lambda (_: T).(drop h (r (Flat f) d0) c2 e))) (ex2 C (\lambda (e1:
 489 C).(drop (S i0) O (CHead c2 (Flat f) t) e1)) (\lambda (e1: C).(drop h (minus
 490 (S d0) (S i0)) e1 e2))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H2: (eq C
 491 c3 (CHead x0 (Flat f) x1))).(\lambda (H3: (eq T t (lift h (r (Flat f) d0)
 492 x1))).(\lambda (H4: (drop h (r (Flat f) d0) c2 x0)).(let H5 \def (eq_ind C c3
 493 (\lambda (c: C).(drop (S i0) O c e2)) H1 (CHead x0 (Flat f) x1) H2) in
 494 (eq_ind_r T (lift h (r (Flat f) d0) x1) (\lambda (t0: T).(ex2 C (\lambda (e1:
 495 C).(drop (S i0) O (CHead c2 (Flat f) t0) e1)) (\lambda (e1: C).(drop h (minus
 496 (S d0) (S i0)) e1 e2)))) (ex2_ind C (\lambda (e1: C).(drop (S i0) O c2 e1))
 497 (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2)) (ex2 C (\lambda (e1:
 498 C).(drop (S i0) O (CHead c2 (Flat f) (lift h (r (Flat f) d0) x1)) e1))
 499 (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2))) (\lambda (x:
 500 C).(\lambda (H6: (drop (S i0) O c2 x)).(\lambda (H7: (drop h (minus (S d0) (S
 501 i0)) x e2)).(ex_intro2 C (\lambda (e1: C).(drop (S i0) O (CHead c2 (Flat f)
 502 (lift h (r (Flat f) d0) x1)) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S
 503 i0)) e1 e2)) x (drop_drop (Flat f) i0 c2 x H6 (lift h (r (Flat f) d0) x1))
 504 H7)))) (IHc x0 h H4 e2 (drop_gen_drop (Flat f) x0 e2 x1 i0 H5))) t H3)))))))
 505 (drop_gen_skip_l c2 c3 t h d0 (Flat f) H0))))))))) k)))) c1))))) d)))) i).
 506
 507 theorem drop_trans_ge:
 508  \forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (d:
 509 nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((drop i O c2
 510 e2) \to ((le d i) \to (drop (plus i h) O c1 e2)))))))))
 511 \def
 512  \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (c2:
 513 C).(\forall (d: nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2:
 514 C).((drop n O c2 e2) \to ((le d n) \to (drop (plus n h) O c1 e2))))))))))
 515 (\lambda (c1: C).(\lambda (c2: C).(\lambda (d: nat).(\lambda (h:
 516 nat).(\lambda (H: (drop h d c1 c2)).(\lambda (e2: C).(\lambda (H0: (drop O O
 517 c2 e2)).(\lambda (H1: (le d O)).(eq_ind C c2 (\lambda (c: C).(drop (plus O h)
 518 O c1 c)) (let H_y \def (le_n_O_eq d H1) in (let H2 \def (eq_ind_r nat d
 519 (\lambda (n: nat).(drop h n c1 c2)) H O H_y) in H2)) e2 (drop_gen_refl c2 e2
 520 H0)))))))))) (\lambda (i0: nat).(\lambda (IHi: ((\forall (c1: C).(\forall
 521 (c2: C).(\forall (d: nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall
 522 (e2: C).((drop i0 O c2 e2) \to ((le d i0) \to (drop (plus i0 h) O c1
 523 e2))))))))))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2:
 524 C).(\forall (d: nat).(\forall (h: nat).((drop h d c c2) \to (\forall (e2:
 525 C).((drop (S i0) O c2 e2) \to ((le d (S i0)) \to (drop (plus (S i0) h) O c
 526 e2))))))))) (\lambda (n: nat).(\lambda (c2: C).(\lambda (d: nat).(\lambda (h:
 527 nat).(\lambda (H: (drop h d (CSort n) c2)).(\lambda (e2: C).(\lambda (H0:
 528 (drop (S i0) O c2 e2)).(\lambda (H1: (le d (S i0))).(and3_ind (eq C c2 (CSort
 529 n)) (eq nat h O) (eq nat d O) (drop (S (plus i0 h)) O (CSort n) e2) (\lambda
 530 (H2: (eq C c2 (CSort n))).(\lambda (H3: (eq nat h O)).(\lambda (H4: (eq nat d
 531 O)).(eq_ind_r nat O (\lambda (n0: nat).(drop (S (plus i0 n0)) O (CSort n)
 532 e2)) (let H5 \def (eq_ind nat d (\lambda (n0: nat).(le n0 (S i0))) H1 O H4)
 533 in (let H6 \def (eq_ind C c2 (\lambda (c: C).(drop (S i0) O c e2)) H0 (CSort
 534 n) H2) in (and3_ind (eq C e2 (CSort n)) (eq nat (S i0) O) (eq nat O O) (drop
 535 (S (plus i0 O)) O (CSort n) e2) (\lambda (H7: (eq C e2 (CSort n))).(\lambda
 536 (H8: (eq nat (S i0) O)).(\lambda (_: (eq nat O O)).(eq_ind_r C (CSort n)
 537 (\lambda (c: C).(drop (S (plus i0 O)) O (CSort n) c)) (let H10 \def (eq_ind
 538 nat (S i0) (\lambda (ee: nat).(match ee with [O \Rightarrow False | (S _)
 539 \Rightarrow True])) I O H8) in (False_ind (drop (S (plus i0 O)) O (CSort n)
 540 (CSort n)) H10)) e2 H7)))) (drop_gen_sort n (S i0) O e2 H6)))) h H3))))
 541 (drop_gen_sort n h d c2 H)))))))))) (\lambda (c2: C).(\lambda (IHc: ((\forall
 542 (c3: C).(\forall (d: nat).(\forall (h: nat).((drop h d c2 c3) \to (\forall
 543 (e2: C).((drop (S i0) O c3 e2) \to ((le d (S i0)) \to (drop (S (plus i0 h)) O
 544 c2 e2)))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c3: C).(\lambda (d:
 545 nat).(nat_ind (\lambda (n: nat).(\forall (h: nat).((drop h n (CHead c2 k t)
 546 c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to ((le n (S i0)) \to (drop
 547 (S (plus i0 h)) O (CHead c2 k t) e2))))))) (\lambda (h: nat).(nat_ind
 548 (\lambda (n: nat).((drop n O (CHead c2 k t) c3) \to (\forall (e2: C).((drop
 549 (S i0) O c3 e2) \to ((le O (S i0)) \to (drop (S (plus i0 n)) O (CHead c2 k t)
 550 e2)))))) (\lambda (H: (drop O O (CHead c2 k t) c3)).(\lambda (e2: C).(\lambda
 551 (H0: (drop (S i0) O c3 e2)).(\lambda (_: (le O (S i0))).(let H2 \def
 552 (eq_ind_r C c3 (\lambda (c: C).(drop (S i0) O c e2)) H0 (CHead c2 k t)
 553 (drop_gen_refl (CHead c2 k t) c3 H)) in (eq_ind nat i0 (\lambda (n:
 554 nat).(drop (S n) O (CHead c2 k t) e2)) (drop_drop k i0 c2 e2 (drop_gen_drop k
 555 c2 e2 t i0 H2) t) (plus i0 O) (plus_n_O i0))))))) (\lambda (n: nat).(\lambda
 556 (_: (((drop n O (CHead c2 k t) c3) \to (\forall (e2: C).((drop (S i0) O c3
 557 e2) \to ((le O (S i0)) \to (drop (S (plus i0 n)) O (CHead c2 k t)
 558 e2))))))).(\lambda (H0: (drop (S n) O (CHead c2 k t) c3)).(\lambda (e2:
 559 C).(\lambda (H1: (drop (S i0) O c3 e2)).(\lambda (H2: (le O (S i0))).(eq_ind
 560 nat (S (plus i0 n)) (\lambda (n0: nat).(drop (S n0) O (CHead c2 k t) e2))
 561 (drop_drop k (S (plus i0 n)) c2 e2 (eq_ind_r nat (S (r k (plus i0 n)))
 562 (\lambda (n0: nat).(drop n0 O c2 e2)) (eq_ind_r nat (plus i0 (r k n))
 563 (\lambda (n0: nat).(drop (S n0) O c2 e2)) (IHc c3 O (r k n) (drop_gen_drop k
 564 c2 c3 t n H0) e2 H1 H2) (r k (plus i0 n)) (r_plus_sym k i0 n)) (r k (S (plus
 565 i0 n))) (r_S k (plus i0 n))) t) (plus i0 (S n)) (plus_n_Sm i0 n)))))))) h))
 566 (\lambda (d0: nat).(\lambda (IHd: ((\forall (h: nat).((drop h d0 (CHead c2 k
 567 t) c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to ((le d0 (S i0)) \to
 568 (drop (S (plus i0 h)) O (CHead c2 k t) e2)))))))).(\lambda (h: nat).(\lambda
 569 (H: (drop h (S d0) (CHead c2 k t) c3)).(\lambda (e2: C).(\lambda (H0: (drop
 570 (S i0) O c3 e2)).(\lambda (H1: (le (S d0) (S i0))).(ex3_2_ind C T (\lambda
 571 (e: C).(\lambda (v: T).(eq C c3 (CHead e k v)))) (\lambda (_: C).(\lambda (v:
 572 T).(eq T t (lift h (r k d0) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r
 573 k d0) c2 e))) (drop (S (plus i0 h)) O (CHead c2 k t) e2) (\lambda (x0:
 574 C).(\lambda (x1: T).(\lambda (H2: (eq C c3 (CHead x0 k x1))).(\lambda (H3:
 575 (eq T t (lift h (r k d0) x1))).(\lambda (H4: (drop h (r k d0) c2 x0)).(let H5
 576 \def (eq_ind C c3 (\lambda (c: C).(\forall (h0: nat).((drop h0 d0 (CHead c2 k
 577 t) c) \to (\forall (e3: C).((drop (S i0) O c e3) \to ((le d0 (S i0)) \to
 578 (drop (S (plus i0 h0)) O (CHead c2 k t) e3))))))) IHd (CHead x0 k x1) H2) in
 579 (let H6 \def (eq_ind C c3 (\lambda (c: C).(drop (S i0) O c e2)) H0 (CHead x0
 580 k x1) H2) in (let H7 \def (eq_ind T t (\lambda (t0: T).(\forall (h0:
 581 nat).((drop h0 d0 (CHead c2 k t0) (CHead x0 k x1)) \to (\forall (e3:
 582 C).((drop (S i0) O (CHead x0 k x1) e3) \to ((le d0 (S i0)) \to (drop (S (plus
 583 i0 h0)) O (CHead c2 k t0) e3))))))) H5 (lift h (r k d0) x1) H3) in (eq_ind_r
 584 T (lift h (r k d0) x1) (\lambda (t0: T).(drop (S (plus i0 h)) O (CHead c2 k
 585 t0) e2)) (drop_drop k (plus i0 h) c2 e2 (K_ind (\lambda (k0: K).((drop h (r
 586 k0 d0) c2 x0) \to ((drop (r k0 i0) O x0 e2) \to (drop (r k0 (plus i0 h)) O c2
 587 e2)))) (\lambda (b: B).(\lambda (H8: (drop h (r (Bind b) d0) c2 x0)).(\lambda
 588 (H9: (drop (r (Bind b) i0) O x0 e2)).(IHi c2 x0 (r (Bind b) d0) h H8 e2 H9
 589 (le_S_n (r (Bind b) d0) i0 H1))))) (\lambda (f: F).(\lambda (H8: (drop h (r
 590 (Flat f) d0) c2 x0)).(\lambda (H9: (drop (r (Flat f) i0) O x0 e2)).(IHc x0 (r
 591 (Flat f) d0) h H8 e2 H9 H1)))) k H4 (drop_gen_drop k x0 e2 x1 i0 H6)) (lift h
 592 (r k d0) x1)) t H3))))))))) (drop_gen_skip_l c2 c3 t h d0 k H)))))))))
 593 d))))))) c1)))) i).
 594