matita/matita/contribs/lambdadelta/basic_1/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-1/drop/fwd.ma".
  18
  19 include "Basic-1/lift/props.ma".
  20
  21 include "Basic-1/r/props.ma".
  22
  23 theorem drop_skip_bind:
  24  \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h
  25 d c e) \to (\forall (b: B).(\forall (u: T).(drop h (S d) (CHead c (Bind b)
  26 (lift h d u)) (CHead e (Bind b) u))))))))
  27 \def
  28  \lambda (h: nat).(\lambda (d: nat).(\lambda (c: C).(\lambda (e: C).(\lambda
  29 (H: (drop h d c e)).(\lambda (b: B).(\lambda (u: T).(eq_ind nat (r (Bind b)
  30 d) (\lambda (n: nat).(drop h (S d) (CHead c (Bind b) (lift h n u)) (CHead e
  31 (Bind b) u))) (drop_skip (Bind b) h d c e H u) d (refl_equal nat d)))))))).
  32 (* COMMENTS
  33 Initial nodes: 95
  34 END *)
  35
  36 theorem drop_skip_flat:
  37  \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h
  38 (S d) c e) \to (\forall (f: F).(\forall (u: T).(drop h (S d) (CHead c (Flat
  39 f) (lift h (S d) u)) (CHead e (Flat f) u))))))))
  40 \def
  41  \lambda (h: nat).(\lambda (d: nat).(\lambda (c: C).(\lambda (e: C).(\lambda
  42 (H: (drop h (S d) c e)).(\lambda (f: F).(\lambda (u: T).(eq_ind nat (r (Flat
  43 f) d) (\lambda (n: nat).(drop h (S d) (CHead c (Flat f) (lift h n u)) (CHead
  44 e (Flat f) u))) (drop_skip (Flat f) h d c e H u) (S d) (refl_equal nat (S
  45 d))))))))).
  46 (* COMMENTS
  47 Initial nodes: 101
  48 END *)
  49
  50 theorem drop_S:
  51  \forall (b: B).(\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (h:
  52 nat).((drop h O c (CHead e (Bind b) u)) \to (drop (S h) O c e))))))
  53 \def
  54  \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e:
  55 C).(\forall (u: T).(\forall (h: nat).((drop h O c0 (CHead e (Bind b) u)) \to
  56 (drop (S h) O c0 e)))))) (\lambda (n: nat).(\lambda (e: C).(\lambda (u:
  57 T).(\lambda (h: nat).(\lambda (H: (drop h O (CSort n) (CHead e (Bind b)
  58 u))).(and3_ind (eq C (CHead e (Bind b) u) (CSort n)) (eq nat h O) (eq nat O
  59 O) (drop (S h) O (CSort n) e) (\lambda (H0: (eq C (CHead e (Bind b) u) (CSort
  60 n))).(\lambda (H1: (eq nat h O)).(\lambda (_: (eq nat O O)).(eq_ind_r nat O
  61 (\lambda (n0: nat).(drop (S n0) O (CSort n) e)) (let H3 \def (eq_ind C (CHead
  62 e (Bind b) u) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop)
  63 with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I
  64 (CSort n) H0) in (False_ind (drop (S O) O (CSort n) e) H3)) h H1))))
  65 (drop_gen_sort n h O (CHead e (Bind b) u) H))))))) (\lambda (c0: C).(\lambda
  66 (H: ((\forall (e: C).(\forall (u: T).(\forall (h: nat).((drop h O c0 (CHead e
  67 (Bind b) u)) \to (drop (S h) O c0 e))))))).(\lambda (k: K).(\lambda (t:
  68 T).(\lambda (e: C).(\lambda (u: T).(\lambda (h: nat).(nat_ind (\lambda (n:
  69 nat).((drop n O (CHead c0 k t) (CHead e (Bind b) u)) \to (drop (S n) O (CHead
  70 c0 k t) e))) (\lambda (H0: (drop O O (CHead c0 k t) (CHead e (Bind b)
  71 u))).(let H1 \def (f_equal C C (\lambda (e0: C).(match e0 in C return
  72 (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c1 _ _)
  73 \Rightarrow c1])) (CHead c0 k t) (CHead e (Bind b) u) (drop_gen_refl (CHead
  74 c0 k t) (CHead e (Bind b) u) H0)) in ((let H2 \def (f_equal C K (\lambda (e0:
  75 C).(match e0 in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k |
  76 (CHead _ k0 _) \Rightarrow k0])) (CHead c0 k t) (CHead e (Bind b) u)
  77 (drop_gen_refl (CHead c0 k t) (CHead e (Bind b) u) H0)) in ((let H3 \def
  78 (f_equal C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) with
  79 [(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0])) (CHead c0 k t)
  80 (CHead e (Bind b) u) (drop_gen_refl (CHead c0 k t) (CHead e (Bind b) u) H0))
  81 in (\lambda (H4: (eq K k (Bind b))).(\lambda (H5: (eq C c0 e)).(eq_ind C c0
  82 (\lambda (c1: C).(drop (S O) O (CHead c0 k t) c1)) (eq_ind_r K (Bind b)
  83 (\lambda (k0: K).(drop (S O) O (CHead c0 k0 t) c0)) (drop_drop (Bind b) O c0
  84 c0 (drop_refl c0) t) k H4) e H5)))) H2)) H1))) (\lambda (n: nat).(\lambda (_:
  85 (((drop n O (CHead c0 k t) (CHead e (Bind b) u)) \to (drop (S n) O (CHead c0
  86 k t) e)))).(\lambda (H1: (drop (S n) O (CHead c0 k t) (CHead e (Bind b)
  87 u))).(drop_drop k (S n) c0 e (eq_ind_r nat (S (r k n)) (\lambda (n0:
  88 nat).(drop n0 O c0 e)) (H e u (r k n) (drop_gen_drop k c0 (CHead e (Bind b)
  89 u) t n H1)) (r k (S n)) (r_S k n)) t)))) h)))))))) c)).
  90 (* COMMENTS
  91 Initial nodes: 807
  92 END *)
  93
  94 theorem drop_ctail:
  95  \forall (c1: C).(\forall (c2: C).(\forall (d: nat).(\forall (h: nat).((drop
  96 h d c1 c2) \to (\forall (k: K).(\forall (u: T).(drop h d (CTail k u c1)
  97 (CTail k u c2))))))))
  98 \def
  99  \lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).(\forall (d:
 100 nat).(\forall (h: nat).((drop h d c c2) \to (\forall (k: K).(\forall (u:
 101 T).(drop h d (CTail k u c) (CTail k u c2))))))))) (\lambda (n: nat).(\lambda
 102 (c2: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H: (drop h d (CSort n)
 103 c2)).(\lambda (k: K).(\lambda (u: T).(and3_ind (eq C c2 (CSort n)) (eq nat h
 104 O) (eq nat d O) (drop h d (CTail k u (CSort n)) (CTail k u c2)) (\lambda (H0:
 105 (eq C c2 (CSort n))).(\lambda (H1: (eq nat h O)).(\lambda (H2: (eq nat d
 106 O)).(eq_ind_r nat O (\lambda (n0: nat).(drop n0 d (CTail k u (CSort n))
 107 (CTail k u c2))) (eq_ind_r nat O (\lambda (n0: nat).(drop O n0 (CTail k u
 108 (CSort n)) (CTail k u c2))) (eq_ind_r C (CSort n) (\lambda (c: C).(drop O O
 109 (CTail k u (CSort n)) (CTail k u c))) (drop_refl (CTail k u (CSort n))) c2
 110 H0) d H2) h H1)))) (drop_gen_sort n h d c2 H))))))))) (\lambda (c2:
 111 C).(\lambda (IHc: ((\forall (c3: C).(\forall (d: nat).(\forall (h:
 112 nat).((drop h d c2 c3) \to (\forall (k: K).(\forall (u: T).(drop h d (CTail k
 113 u c2) (CTail k u c3)))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c3:
 114 C).(\lambda (d: nat).(nat_ind (\lambda (n: nat).(\forall (h: nat).((drop h n
 115 (CHead c2 k t) c3) \to (\forall (k0: K).(\forall (u: T).(drop h n (CTail k0 u
 116 (CHead c2 k t)) (CTail k0 u c3))))))) (\lambda (h: nat).(nat_ind (\lambda (n:
 117 nat).((drop n O (CHead c2 k t) c3) \to (\forall (k0: K).(\forall (u: T).(drop
 118 n O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)))))) (\lambda (H: (drop O O
 119 (CHead c2 k t) c3)).(\lambda (k0: K).(\lambda (u: T).(eq_ind C (CHead c2 k t)
 120 (\lambda (c: C).(drop O O (CTail k0 u (CHead c2 k t)) (CTail k0 u c)))
 121 (drop_refl (CTail k0 u (CHead c2 k t))) c3 (drop_gen_refl (CHead c2 k t) c3
 122 H))))) (\lambda (n: nat).(\lambda (_: (((drop n O (CHead c2 k t) c3) \to
 123 (\forall (k0: K).(\forall (u: T).(drop n O (CTail k0 u (CHead c2 k t)) (CTail
 124 k0 u c3))))))).(\lambda (H0: (drop (S n) O (CHead c2 k t) c3)).(\lambda (k0:
 125 K).(\lambda (u: T).(drop_drop k n (CTail k0 u c2) (CTail k0 u c3) (IHc c3 O
 126 (r k n) (drop_gen_drop k c2 c3 t n H0) k0 u) t)))))) h)) (\lambda (n:
 127 nat).(\lambda (H: ((\forall (h: nat).((drop h n (CHead c2 k t) c3) \to
 128 (\forall (k0: K).(\forall (u: T).(drop h n (CTail k0 u (CHead c2 k t)) (CTail
 129 k0 u c3)))))))).(\lambda (h: nat).(\lambda (H0: (drop h (S n) (CHead c2 k t)
 130 c3)).(\lambda (k0: K).(\lambda (u: T).(ex3_2_ind C T (\lambda (e: C).(\lambda
 131 (v: T).(eq C c3 (CHead e k v)))) (\lambda (_: C).(\lambda (v: T).(eq T t
 132 (lift h (r k n) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r k n) c2 e)))
 133 (drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)) (\lambda (x0:
 134 C).(\lambda (x1: T).(\lambda (H1: (eq C c3 (CHead x0 k x1))).(\lambda (H2:
 135 (eq T t (lift h (r k n) x1))).(\lambda (H3: (drop h (r k n) c2 x0)).(let H4
 136 \def (eq_ind C c3 (\lambda (c: C).(\forall (h0: nat).((drop h0 n (CHead c2 k
 137 t) c) \to (\forall (k1: K).(\forall (u0: T).(drop h0 n (CTail k1 u0 (CHead c2
 138 k t)) (CTail k1 u0 c))))))) H (CHead x0 k x1) H1) in (eq_ind_r C (CHead x0 k
 139 x1) (\lambda (c: C).(drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u
 140 c))) (let H5 \def (eq_ind T t (\lambda (t0: T).(\forall (h0: nat).((drop h0 n
 141 (CHead c2 k t0) (CHead x0 k x1)) \to (\forall (k1: K).(\forall (u0: T).(drop
 142 h0 n (CTail k1 u0 (CHead c2 k t0)) (CTail k1 u0 (CHead x0 k x1)))))))) H4
 143 (lift h (r k n) x1) H2) in (eq_ind_r T (lift h (r k n) x1) (\lambda (t0:
 144 T).(drop h (S n) (CTail k0 u (CHead c2 k t0)) (CTail k0 u (CHead x0 k x1))))
 145 (drop_skip k h n (CTail k0 u c2) (CTail k0 u x0) (IHc x0 (r k n) h H3 k0 u)
 146 x1) t H2)) c3 H1))))))) (drop_gen_skip_l c2 c3 t h n k H0)))))))) d)))))))
 147 c1).
 148 (* COMMENTS
 149 Initial nodes: 1211
 150 END *)
 151
 152 theorem drop_mono:
 153  \forall (c: C).(\forall (x1: C).(\forall (d: nat).(\forall (h: nat).((drop h
 154 d c x1) \to (\forall (x2: C).((drop h d c x2) \to (eq C x1 x2)))))))
 155 \def
 156  \lambda (c: C).(C_ind (\lambda (c0: C).(\forall (x1: C).(\forall (d:
 157 nat).(\forall (h: nat).((drop h d c0 x1) \to (\forall (x2: C).((drop h d c0
 158 x2) \to (eq C x1 x2)))))))) (\lambda (n: nat).(\lambda (x1: C).(\lambda (d:
 159 nat).(\lambda (h: nat).(\lambda (H: (drop h d (CSort n) x1)).(\lambda (x2:
 160 C).(\lambda (H0: (drop h d (CSort n) x2)).(and3_ind (eq C x2 (CSort n)) (eq
 161 nat h O) (eq nat d O) (eq C x1 x2) (\lambda (H1: (eq C x2 (CSort
 162 n))).(\lambda (H2: (eq nat h O)).(\lambda (H3: (eq nat d O)).(and3_ind (eq C
 163 x1 (CSort n)) (eq nat h O) (eq nat d O) (eq C x1 x2) (\lambda (H4: (eq C x1
 164 (CSort n))).(\lambda (H5: (eq nat h O)).(\lambda (H6: (eq nat d O)).(eq_ind_r
 165 C (CSort n) (\lambda (c0: C).(eq C x1 c0)) (let H7 \def (eq_ind nat h
 166 (\lambda (n0: nat).(eq nat n0 O)) H2 O H5) in (let H8 \def (eq_ind nat d
 167 (\lambda (n0: nat).(eq nat n0 O)) H3 O H6) in (eq_ind_r C (CSort n) (\lambda
 168 (c0: C).(eq C c0 (CSort n))) (refl_equal C (CSort n)) x1 H4))) x2 H1))))
 169 (drop_gen_sort n h d x1 H))))) (drop_gen_sort n h d x2 H0))))))))) (\lambda
 170 (c0: C).(\lambda (H: ((\forall (x1: C).(\forall (d: nat).(\forall (h:
 171 nat).((drop h d c0 x1) \to (\forall (x2: C).((drop h d c0 x2) \to (eq C x1
 172 x2))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (x1: C).(\lambda (d:
 173 nat).(nat_ind (\lambda (n: nat).(\forall (h: nat).((drop h n (CHead c0 k t)
 174 x1) \to (\forall (x2: C).((drop h n (CHead c0 k t) x2) \to (eq C x1 x2))))))
 175 (\lambda (h: nat).(nat_ind (\lambda (n: nat).((drop n O (CHead c0 k t) x1)
 176 \to (\forall (x2: C).((drop n O (CHead c0 k t) x2) \to (eq C x1 x2)))))
 177 (\lambda (H0: (drop O O (CHead c0 k t) x1)).(\lambda (x2: C).(\lambda (H1:
 178 (drop O O (CHead c0 k t) x2)).(eq_ind C (CHead c0 k t) (\lambda (c1: C).(eq C
 179 x1 c1)) (eq_ind C (CHead c0 k t) (\lambda (c1: C).(eq C c1 (CHead c0 k t)))
 180 (refl_equal C (CHead c0 k t)) x1 (drop_gen_refl (CHead c0 k t) x1 H0)) x2
 181 (drop_gen_refl (CHead c0 k t) x2 H1))))) (\lambda (n: nat).(\lambda (_:
 182 (((drop n O (CHead c0 k t) x1) \to (\forall (x2: C).((drop n O (CHead c0 k t)
 183 x2) \to (eq C x1 x2)))))).(\lambda (H1: (drop (S n) O (CHead c0 k t)
 184 x1)).(\lambda (x2: C).(\lambda (H2: (drop (S n) O (CHead c0 k t) x2)).(H x1 O
 185 (r k n) (drop_gen_drop k c0 x1 t n H1) x2 (drop_gen_drop k c0 x2 t n
 186 H2))))))) h)) (\lambda (n: nat).(\lambda (H0: ((\forall (h: nat).((drop h n
 187 (CHead c0 k t) x1) \to (\forall (x2: C).((drop h n (CHead c0 k t) x2) \to (eq
 188 C x1 x2))))))).(\lambda (h: nat).(\lambda (H1: (drop h (S n) (CHead c0 k t)
 189 x1)).(\lambda (x2: C).(\lambda (H2: (drop h (S n) (CHead c0 k t)
 190 x2)).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C x2 (CHead e k v))))
 191 (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k n) v)))) (\lambda (e:
 192 C).(\lambda (_: T).(drop h (r k n) c0 e))) (eq C x1 x2) (\lambda (x0:
 193 C).(\lambda (x3: T).(\lambda (H3: (eq C x2 (CHead x0 k x3))).(\lambda (H4:
 194 (eq T t (lift h (r k n) x3))).(\lambda (H5: (drop h (r k n) c0
 195 x0)).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C x1 (CHead e k v))))
 196 (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k n) v)))) (\lambda (e:
 197 C).(\lambda (_: T).(drop h (r k n) c0 e))) (eq C x1 x2) (\lambda (x4:
 198 C).(\lambda (x5: T).(\lambda (H6: (eq C x1 (CHead x4 k x5))).(\lambda (H7:
 199 (eq T t (lift h (r k n) x5))).(\lambda (H8: (drop h (r k n) c0 x4)).(eq_ind_r
 200 C (CHead x0 k x3) (\lambda (c1: C).(eq C x1 c1)) (let H9 \def (eq_ind C x1
 201 (\lambda (c1: C).(\forall (h0: nat).((drop h0 n (CHead c0 k t) c1) \to
 202 (\forall (x6: C).((drop h0 n (CHead c0 k t) x6) \to (eq C c1 x6)))))) H0
 203 (CHead x4 k x5) H6) in (eq_ind_r C (CHead x4 k x5) (\lambda (c1: C).(eq C c1
 204 (CHead x0 k x3))) (let H10 \def (eq_ind T t (\lambda (t0: T).(\forall (h0:
 205 nat).((drop h0 n (CHead c0 k t0) (CHead x4 k x5)) \to (\forall (x6: C).((drop
 206 h0 n (CHead c0 k t0) x6) \to (eq C (CHead x4 k x5) x6)))))) H9 (lift h (r k
 207 n) x5) H7) in (let H11 \def (eq_ind T t (\lambda (t0: T).(eq T t0 (lift h (r
 208 k n) x3))) H4 (lift h (r k n) x5) H7) in (let H12 \def (eq_ind T x5 (\lambda
 209 (t0: T).(\forall (h0: nat).((drop h0 n (CHead c0 k (lift h (r k n) t0))
 210 (CHead x4 k t0)) \to (\forall (x6: C).((drop h0 n (CHead c0 k (lift h (r k n)
 211 t0)) x6) \to (eq C (CHead x4 k t0) x6)))))) H10 x3 (lift_inj x5 x3 h (r k n)
 212 H11)) in (eq_ind_r T x3 (\lambda (t0: T).(eq C (CHead x4 k t0) (CHead x0 k
 213 x3))) (f_equal3 C K T C CHead x4 x0 k k x3 x3 (sym_eq C x0 x4 (H x0 (r k n) h
 214 H5 x4 H8)) (refl_equal K k) (refl_equal T x3)) x5 (lift_inj x5 x3 h (r k n)
 215 H11))))) x1 H6)) x2 H3)))))) (drop_gen_skip_l c0 x1 t h n k H1)))))))
 216 (drop_gen_skip_l c0 x2 t h n k H2)))))))) d))))))) c).
 217 (* COMMENTS
 218 Initial nodes: 1539
 219 END *)
 220
 221 theorem drop_conf_lt:
 222  \forall (k: K).(\forall (i: nat).(\forall (u: T).(\forall (c0: C).(\forall
 223 (c: C).((drop i O c (CHead c0 k u)) \to (\forall (e: C).(\forall (h:
 224 nat).(\forall (d: nat).((drop h (S (plus i d)) c e) \to (ex3_2 T C (\lambda
 225 (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 226 (e0: C).(drop i O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop
 227 h (r k d) c0 e0)))))))))))))
 228 \def
 229  \lambda (k: K).(\lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (u:
 230 T).(\forall (c0: C).(\forall (c: C).((drop n O c (CHead c0 k u)) \to (\forall
 231 (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus n d)) c e) \to
 232 (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v))))
 233 (\lambda (v: T).(\lambda (e0: C).(drop n O e (CHead e0 k v)))) (\lambda (_:
 234 T).(\lambda (e0: C).(drop h (r k d) c0 e0))))))))))))) (\lambda (u:
 235 T).(\lambda (c0: C).(\lambda (c: C).(\lambda (H: (drop O O c (CHead c0 k
 236 u))).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H0: (drop
 237 h (S (plus O d)) c e)).(let H1 \def (eq_ind C c (\lambda (c1: C).(drop h (S
 238 (plus O d)) c1 e)) H0 (CHead c0 k u) (drop_gen_refl c (CHead c0 k u) H)) in
 239 (ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 k v))))
 240 (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k (plus O d)) v))))
 241 (\lambda (e0: C).(\lambda (_: T).(drop h (r k (plus O d)) c0 e0))) (ex3_2 T C
 242 (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v:
 243 T).(\lambda (e0: C).(drop O O e (CHead e0 k v)))) (\lambda (_: T).(\lambda
 244 (e0: C).(drop h (r k d) c0 e0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda
 245 (H2: (eq C e (CHead x0 k x1))).(\lambda (H3: (eq T u (lift h (r k (plus O d))
 246 x1))).(\lambda (H4: (drop h (r k (plus O d)) c0 x0)).(eq_ind_r C (CHead x0 k
 247 x1) (\lambda (c1: C).(ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift
 248 h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop O O c1 (CHead e0 k
 249 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))) (eq_ind_r T
 250 (lift h (r k (plus O d)) x1) (\lambda (t: T).(ex3_2 T C (\lambda (v:
 251 T).(\lambda (_: C).(eq T t (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 252 (e0: C).(drop O O (CHead x0 k x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda
 253 (e0: C).(drop h (r k d) c0 e0))))) (ex3_2_intro T C (\lambda (v: T).(\lambda
 254 (_: C).(eq T (lift h (r k (plus O d)) x1) (lift h (r k d) v)))) (\lambda (v:
 255 T).(\lambda (e0: C).(drop O O (CHead x0 k x1) (CHead e0 k v)))) (\lambda (_:
 256 T).(\lambda (e0: C).(drop h (r k d) c0 e0))) x1 x0 (refl_equal T (lift h (r k
 257 d) x1)) (drop_refl (CHead x0 k x1)) H4) u H3) e H2)))))) (drop_gen_skip_l c0
 258 e u h (plus O d) k H1))))))))))) (\lambda (i0: nat).(\lambda (H: ((\forall
 259 (u: T).(\forall (c0: C).(\forall (c: C).((drop i0 O c (CHead c0 k u)) \to
 260 (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus i0 d))
 261 c e) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d)
 262 v)))) (\lambda (v: T).(\lambda (e0: C).(drop i0 O e (CHead e0 k v))))
 263 (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))))))))))))).(\lambda
 264 (u: T).(\lambda (c0: C).(\lambda (c: C).(C_ind (\lambda (c1: C).((drop (S i0)
 265 O c1 (CHead c0 k u)) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
 266 nat).((drop h (S (plus (S i0) d)) c1 e) \to (ex3_2 T C (\lambda (v:
 267 T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 268 (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
 269 C).(drop h (r k d) c0 e0)))))))))) (\lambda (n: nat).(\lambda (_: (drop (S
 270 i0) O (CSort n) (CHead c0 k u))).(\lambda (e: C).(\lambda (h: nat).(\lambda
 271 (d: nat).(\lambda (H1: (drop h (S (plus (S i0) d)) (CSort n) e)).(and3_ind
 272 (eq C e (CSort n)) (eq nat h O) (eq nat (S (plus (S i0) d)) O) (ex3_2 T C
 273 (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v:
 274 T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_:
 275 T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) (\lambda (_: (eq C e (CSort
 276 n))).(\lambda (_: (eq nat h O)).(\lambda (H4: (eq nat (S (plus (S i0) d))
 277 O)).(let H5 \def (eq_ind nat (S (plus (S i0) d)) (\lambda (ee: nat).(match ee
 278 in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
 279 \Rightarrow True])) I O H4) in (False_ind (ex3_2 T C (\lambda (v: T).(\lambda
 280 (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop
 281 (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d)
 282 c0 e0)))) H5))))) (drop_gen_sort n h (S (plus (S i0) d)) e H1))))))))
 283 (\lambda (c1: C).(\lambda (H0: (((drop (S i0) O c1 (CHead c0 k u)) \to
 284 (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus (S i0)
 285 d)) c1 e) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k
 286 d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k v))))
 287 (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))))))))).(\lambda
 288 (k0: K).(K_ind (\lambda (k1: K).(\forall (t: T).((drop (S i0) O (CHead c1 k1
 289 t) (CHead c0 k u)) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
 290 nat).((drop h (S (plus (S i0) d)) (CHead c1 k1 t) e) \to (ex3_2 T C (\lambda
 291 (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 292 (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
 293 C).(drop h (r k d) c0 e0))))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda
 294 (H1: (drop (S i0) O (CHead c1 (Bind b) t) (CHead c0 k u))).(\lambda (e:
 295 C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H2: (drop h (S (plus (S i0)
 296 d)) (CHead c1 (Bind b) t) e)).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v:
 297 T).(eq C e (CHead e0 (Bind b) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t
 298 (lift h (r (Bind b) (plus (S i0) d)) v)))) (\lambda (e0: C).(\lambda (_:
 299 T).(drop h (r (Bind b) (plus (S i0) d)) c1 e0))) (ex3_2 T C (\lambda (v:
 300 T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 301 (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
 302 C).(drop h (r k d) c0 e0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H3:
 303 (eq C e (CHead x0 (Bind b) x1))).(\lambda (_: (eq T t (lift h (r (Bind b)
 304 (plus (S i0) d)) x1))).(\lambda (H5: (drop h (r (Bind b) (plus (S i0) d)) c1
 305 x0)).(eq_ind_r C (CHead x0 (Bind b) x1) (\lambda (c2: C).(ex3_2 T C (\lambda
 306 (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 307 (e0: C).(drop (S i0) O c2 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
 308 C).(drop h (r k d) c0 e0))))) (let H6 \def (H u c0 c1 (drop_gen_drop (Bind b)
 309 c1 (CHead c0 k u) t i0 H1) x0 h d H5) in (ex3_2_ind T C (\lambda (v:
 310 T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 311 (e0: C).(drop i0 O x0 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
 312 C).(drop h (r k d) c0 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T
 313 u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O
 314 (CHead x0 (Bind b) x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
 315 C).(drop h (r k d) c0 e0)))) (\lambda (x2: T).(\lambda (x3: C).(\lambda (H7:
 316 (eq T u (lift h (r k d) x2))).(\lambda (H8: (drop i0 O x0 (CHead x3 k
 317 x2))).(\lambda (H9: (drop h (r k d) c0 x3)).(ex3_2_intro T C (\lambda (v:
 318 T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 319 (e0: C).(drop (S i0) O (CHead x0 (Bind b) x1) (CHead e0 k v)))) (\lambda (_:
 320 T).(\lambda (e0: C).(drop h (r k d) c0 e0))) x2 x3 H7 (drop_drop (Bind b) i0
 321 x0 (CHead x3 k x2) H8 x1) H9)))))) H6)) e H3)))))) (drop_gen_skip_l c1 e t h
 322 (plus (S i0) d) (Bind b) H2))))))))) (\lambda (f: F).(\lambda (t: T).(\lambda
 323 (H1: (drop (S i0) O (CHead c1 (Flat f) t) (CHead c0 k u))).(\lambda (e:
 324 C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H2: (drop h (S (plus (S i0)
 325 d)) (CHead c1 (Flat f) t) e)).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v:
 326 T).(eq C e (CHead e0 (Flat f) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t
 327 (lift h (r (Flat f) (plus (S i0) d)) v)))) (\lambda (e0: C).(\lambda (_:
 328 T).(drop h (r (Flat f) (plus (S i0) d)) c1 e0))) (ex3_2 T C (\lambda (v:
 329 T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 330 (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
 331 C).(drop h (r k d) c0 e0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H3:
 332 (eq C e (CHead x0 (Flat f) x1))).(\lambda (_: (eq T t (lift h (r (Flat f)
 333 (plus (S i0) d)) x1))).(\lambda (H5: (drop h (r (Flat f) (plus (S i0) d)) c1
 334 x0)).(eq_ind_r C (CHead x0 (Flat f) x1) (\lambda (c2: C).(ex3_2 T C (\lambda
 335 (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
 336 (e0: C).(drop (S i0) O c2 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
 337 C).(drop h (r k d) c0 e0))))) (ex3_2_ind T C (\lambda (v: T).(\lambda (_:
 338 C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S
 339 i0) O x0 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d)
 340 c0 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d)
 341 v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Flat f) x1)
 342 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))
 343 (\lambda (x2: T).(\lambda (x3: C).(\lambda (H6: (eq T u (lift h (r k d)
 344 x2))).(\lambda (H7: (drop (S i0) O x0 (CHead x3 k x2))).(\lambda (H8: (drop h
 345 (r k d) c0 x3)).(ex3_2_intro T C (\lambda (v: T).(\lambda (_: C).(eq T u
 346 (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead
 347 x0 (Flat f) x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r
 348 k d) c0 e0))) x2 x3 H6 (drop_drop (Flat f) i0 x0 (CHead x3 k x2) H7 x1)
 349 H8)))))) (H0 (drop_gen_drop (Flat f) c1 (CHead c0 k u) t i0 H1) x0 h d H5)) e
 350 H3)))))) (drop_gen_skip_l c1 e t h (plus (S i0) d) (Flat f) H2)))))))))
 351 k0)))) c)))))) i)).
 352 (* COMMENTS
 353 Initial nodes: 2972
 354 END *)
 355
 356 theorem drop_conf_ge:
 357  \forall (i: nat).(\forall (a: C).(\forall (c: C).((drop i O c a) \to
 358 (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c e) \to ((le
 359 (plus d h) i) \to (drop (minus i h) O e a)))))))))
 360 \def
 361  \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (a: C).(\forall (c:
 362 C).((drop n O c a) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
 363 nat).((drop h d c e) \to ((le (plus d h) n) \to (drop (minus n h) O e
 364 a)))))))))) (\lambda (a: C).(\lambda (c: C).(\lambda (H: (drop O O c
 365 a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H0: (drop h
 366 d c e)).(\lambda (H1: (le (plus d h) O)).(let H2 \def (eq_ind C c (\lambda
 367 (c0: C).(drop h d c0 e)) H0 a (drop_gen_refl c a H)) in (let H_y \def
 368 (le_n_O_eq (plus d h) H1) in (land_ind (eq nat d O) (eq nat h O) (drop (minus
 369 O h) O e a) (\lambda (H3: (eq nat d O)).(\lambda (H4: (eq nat h O)).(let H5
 370 \def (eq_ind nat d (\lambda (n: nat).(drop h n a e)) H2 O H3) in (let H6 \def
 371 (eq_ind nat h (\lambda (n: nat).(drop n O a e)) H5 O H4) in (eq_ind_r nat O
 372 (\lambda (n: nat).(drop (minus O n) O e a)) (eq_ind C a (\lambda (c0:
 373 C).(drop (minus O O) O c0 a)) (drop_refl a) e (drop_gen_refl a e H6)) h
 374 H4))))) (plus_O d h (sym_eq nat O (plus d h) H_y))))))))))))) (\lambda (i0:
 375 nat).(\lambda (H: ((\forall (a: C).(\forall (c: C).((drop i0 O c a) \to
 376 (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c e) \to ((le
 377 (plus d h) i0) \to (drop (minus i0 h) O e a))))))))))).(\lambda (a:
 378 C).(\lambda (c: C).(C_ind (\lambda (c0: C).((drop (S i0) O c0 a) \to (\forall
 379 (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c0 e) \to ((le (plus d
 380 h) (S i0)) \to (drop (minus (S i0) h) O e a)))))))) (\lambda (n:
 381 nat).(\lambda (H0: (drop (S i0) O (CSort n) a)).(\lambda (e: C).(\lambda (h:
 382 nat).(\lambda (d: nat).(\lambda (H1: (drop h d (CSort n) e)).(\lambda (H2:
 383 (le (plus d h) (S i0))).(and3_ind (eq C e (CSort n)) (eq nat h O) (eq nat d
 384 O) (drop (minus (S i0) h) O e a) (\lambda (H3: (eq C e (CSort n))).(\lambda
 385 (H4: (eq nat h O)).(\lambda (H5: (eq nat d O)).(and3_ind (eq C a (CSort n))
 386 (eq nat (S i0) O) (eq nat O O) (drop (minus (S i0) h) O e a) (\lambda (H6:
 387 (eq C a (CSort n))).(\lambda (H7: (eq nat (S i0) O)).(\lambda (_: (eq nat O
 388 O)).(let H9 \def (eq_ind nat d (\lambda (n0: nat).(le (plus n0 h) (S i0))) H2
 389 O H5) in (let H10 \def (eq_ind nat h (\lambda (n0: nat).(le (plus O n0) (S
 390 i0))) H9 O H4) in (eq_ind_r nat O (\lambda (n0: nat).(drop (minus (S i0) n0)
 391 O e a)) (eq_ind_r C (CSort n) (\lambda (c0: C).(drop (minus (S i0) O) O c0
 392 a)) (eq_ind_r C (CSort n) (\lambda (c0: C).(drop (minus (S i0) O) O (CSort n)
 393 c0)) (let H11 \def (eq_ind nat (S i0) (\lambda (ee: nat).(match ee in nat
 394 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
 395 True])) I O H7) in (False_ind (drop (minus (S i0) O) O (CSort n) (CSort n))
 396 H11)) a H6) e H3) h H4)))))) (drop_gen_sort n (S i0) O a H0)))))
 397 (drop_gen_sort n h d e H1))))))))) (\lambda (c0: C).(\lambda (H0: (((drop (S
 398 i0) O c0 a) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h
 399 d c0 e) \to ((le (plus d h) (S i0)) \to (drop (minus (S i0) h) O e
 400 a))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t: T).((drop (S
 401 i0) O (CHead c0 k0 t) a) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
 402 nat).((drop h d (CHead c0 k0 t) e) \to ((le (plus d h) (S i0)) \to (drop
 403 (minus (S i0) h) O e a))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (H1:
 404 (drop (S i0) O (CHead c0 (Bind b) t) a)).(\lambda (e: C).(\lambda (h:
 405 nat).(\lambda (d: nat).(\lambda (H2: (drop h d (CHead c0 (Bind b) t)
 406 e)).(\lambda (H3: (le (plus d h) (S i0))).(nat_ind (\lambda (n: nat).((drop h
 407 n (CHead c0 (Bind b) t) e) \to ((le (plus n h) (S i0)) \to (drop (minus (S
 408 i0) h) O e a)))) (\lambda (H4: (drop h O (CHead c0 (Bind b) t) e)).(\lambda
 409 (H5: (le (plus O h) (S i0))).(nat_ind (\lambda (n: nat).((drop n O (CHead c0
 410 (Bind b) t) e) \to ((le (plus O n) (S i0)) \to (drop (minus (S i0) n) O e
 411 a)))) (\lambda (H6: (drop O O (CHead c0 (Bind b) t) e)).(\lambda (_: (le
 412 (plus O O) (S i0))).(eq_ind C (CHead c0 (Bind b) t) (\lambda (c1: C).(drop
 413 (minus (S i0) O) O c1 a)) (drop_drop (Bind b) i0 c0 a (drop_gen_drop (Bind b)
 414 c0 a t i0 H1) t) e (drop_gen_refl (CHead c0 (Bind b) t) e H6)))) (\lambda
 415 (h0: nat).(\lambda (_: (((drop h0 O (CHead c0 (Bind b) t) e) \to ((le (plus O
 416 h0) (S i0)) \to (drop (minus (S i0) h0) O e a))))).(\lambda (H6: (drop (S h0)
 417 O (CHead c0 (Bind b) t) e)).(\lambda (H7: (le (plus O (S h0)) (S i0))).(H a
 418 c0 (drop_gen_drop (Bind b) c0 a t i0 H1) e h0 O (drop_gen_drop (Bind b) c0 e
 419 t h0 H6) (le_S_n (plus O h0) i0 H7)))))) h H4 H5))) (\lambda (d0:
 420 nat).(\lambda (_: (((drop h d0 (CHead c0 (Bind b) t) e) \to ((le (plus d0 h)
 421 (S i0)) \to (drop (minus (S i0) h) O e a))))).(\lambda (H4: (drop h (S d0)
 422 (CHead c0 (Bind b) t) e)).(\lambda (H5: (le (plus (S d0) h) (S
 423 i0))).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 (Bind
 424 b) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r (Bind b) d0)
 425 v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r (Bind b) d0) c0 e0))) (drop
 426 (minus (S i0) h) O e a) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C
 427 e (CHead x0 (Bind b) x1))).(\lambda (_: (eq T t (lift h (r (Bind b) d0)
 428 x1))).(\lambda (H8: (drop h (r (Bind b) d0) c0 x0)).(eq_ind_r C (CHead x0
 429 (Bind b) x1) (\lambda (c1: C).(drop (minus (S i0) h) O c1 a)) (eq_ind nat (S
 430 (minus i0 h)) (\lambda (n: nat).(drop n O (CHead x0 (Bind b) x1) a))
 431 (drop_drop (Bind b) (minus i0 h) x0 a (H a c0 (drop_gen_drop (Bind b) c0 a t
 432 i0 H1) x0 h d0 H8 (le_S_n (plus d0 h) i0 H5)) x1) (minus (S i0) h)
 433 (minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0 h) i0 H5)))) e
 434 H6)))))) (drop_gen_skip_l c0 e t h d0 (Bind b) H4)))))) d H2 H3)))))))))
 435 (\lambda (f: F).(\lambda (t: T).(\lambda (H1: (drop (S i0) O (CHead c0 (Flat
 436 f) t) a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H2:
 437 (drop h d (CHead c0 (Flat f) t) e)).(\lambda (H3: (le (plus d h) (S
 438 i0))).(nat_ind (\lambda (n: nat).((drop h n (CHead c0 (Flat f) t) e) \to ((le
 439 (plus n h) (S i0)) \to (drop (minus (S i0) h) O e a)))) (\lambda (H4: (drop h
 440 O (CHead c0 (Flat f) t) e)).(\lambda (H5: (le (plus O h) (S i0))).(nat_ind
 441 (\lambda (n: nat).((drop n O (CHead c0 (Flat f) t) e) \to ((le (plus O n) (S
 442 i0)) \to (drop (minus (S i0) n) O e a)))) (\lambda (H6: (drop O O (CHead c0
 443 (Flat f) t) e)).(\lambda (_: (le (plus O O) (S i0))).(eq_ind C (CHead c0
 444 (Flat f) t) (\lambda (c1: C).(drop (minus (S i0) O) O c1 a)) (drop_drop (Flat
 445 f) i0 c0 a (drop_gen_drop (Flat f) c0 a t i0 H1) t) e (drop_gen_refl (CHead
 446 c0 (Flat f) t) e H6)))) (\lambda (h0: nat).(\lambda (_: (((drop h0 O (CHead
 447 c0 (Flat f) t) e) \to ((le (plus O h0) (S i0)) \to (drop (minus (S i0) h0) O
 448 e a))))).(\lambda (H6: (drop (S h0) O (CHead c0 (Flat f) t) e)).(\lambda (H7:
 449 (le (plus O (S h0)) (S i0))).(H0 (drop_gen_drop (Flat f) c0 a t i0 H1) e (S
 450 h0) O (drop_gen_drop (Flat f) c0 e t h0 H6) H7))))) h H4 H5))) (\lambda (d0:
 451 nat).(\lambda (_: (((drop h d0 (CHead c0 (Flat f) t) e) \to ((le (plus d0 h)
 452 (S i0)) \to (drop (minus (S i0) h) O e a))))).(\lambda (H4: (drop h (S d0)
 453 (CHead c0 (Flat f) t) e)).(\lambda (H5: (le (plus (S d0) h) (S
 454 i0))).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 (Flat
 455 f) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r (Flat f) d0)
 456 v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r (Flat f) d0) c0 e0))) (drop
 457 (minus (S i0) h) O e a) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C
 458 e (CHead x0 (Flat f) x1))).(\lambda (_: (eq T t (lift h (r (Flat f) d0)
 459 x1))).(\lambda (H8: (drop h (r (Flat f) d0) c0 x0)).(eq_ind_r C (CHead x0
 460 (Flat f) x1) (\lambda (c1: C).(drop (minus (S i0) h) O c1 a)) (let H9 \def
 461 (eq_ind_r nat (minus (S i0) h) (\lambda (n: nat).(drop n O x0 a)) (H0
 462 (drop_gen_drop (Flat f) c0 a t i0 H1) x0 h (S d0) H8 H5) (S (minus i0 h))
 463 (minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0 h) i0 H5)))) in
 464 (eq_ind nat (S (minus i0 h)) (\lambda (n: nat).(drop n O (CHead x0 (Flat f)
 465 x1) a)) (drop_drop (Flat f) (minus i0 h) x0 a H9 x1) (minus (S i0) h)
 466 (minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0 h) i0 H5))))) e
 467 H6)))))) (drop_gen_skip_l c0 e t h d0 (Flat f) H4)))))) d H2 H3)))))))))
 468 k)))) c))))) i).
 469 (* COMMENTS
 470 Initial nodes: 2726
 471 END *)
 472
 473 theorem drop_conf_rev:
 474  \forall (j: nat).(\forall (e1: C).(\forall (e2: C).((drop j O e1 e2) \to
 475 (\forall (c2: C).(\forall (i: nat).((drop i O c2 e2) \to (ex2 C (\lambda (c1:
 476 C).(drop j O c1 c2)) (\lambda (c1: C).(drop i j c1 e1)))))))))
 477 \def
 478  \lambda (j: nat).(nat_ind (\lambda (n: nat).(\forall (e1: C).(\forall (e2:
 479 C).((drop n O e1 e2) \to (\forall (c2: C).(\forall (i: nat).((drop i O c2 e2)
 480 \to (ex2 C (\lambda (c1: C).(drop n O c1 c2)) (\lambda (c1: C).(drop i n c1
 481 e1)))))))))) (\lambda (e1: C).(\lambda (e2: C).(\lambda (H: (drop O O e1
 482 e2)).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H0: (drop i O c2 e2)).(let
 483 H1 \def (eq_ind_r C e2 (\lambda (c: C).(drop i O c2 c)) H0 e1 (drop_gen_refl
 484 e1 e2 H)) in (ex_intro2 C (\lambda (c1: C).(drop O O c1 c2)) (\lambda (c1:
 485 C).(drop i O c1 e1)) c2 (drop_refl c2) H1)))))))) (\lambda (j0: nat).(\lambda
 486 (IHj: ((\forall (e1: C).(\forall (e2: C).((drop j0 O e1 e2) \to (\forall (c2:
 487 C).(\forall (i: nat).((drop i O c2 e2) \to (ex2 C (\lambda (c1: C).(drop j0 O
 488 c1 c2)) (\lambda (c1: C).(drop i j0 c1 e1))))))))))).(\lambda (e1: C).(C_ind
 489 (\lambda (c: C).(\forall (e2: C).((drop (S j0) O c e2) \to (\forall (c2:
 490 C).(\forall (i: nat).((drop i O c2 e2) \to (ex2 C (\lambda (c1: C).(drop (S
 491 j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 c))))))))) (\lambda (n:
 492 nat).(\lambda (e2: C).(\lambda (H: (drop (S j0) O (CSort n) e2)).(\lambda
 493 (c2: C).(\lambda (i: nat).(\lambda (H0: (drop i O c2 e2)).(and3_ind (eq C e2
 494 (CSort n)) (eq nat (S j0) O) (eq nat O O) (ex2 C (\lambda (c1: C).(drop (S
 495 j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CSort n)))) (\lambda (H1:
 496 (eq C e2 (CSort n))).(\lambda (H2: (eq nat (S j0) O)).(\lambda (_: (eq nat O
 497 O)).(let H4 \def (eq_ind C e2 (\lambda (c: C).(drop i O c2 c)) H0 (CSort n)
 498 H1) in (let H5 \def (eq_ind nat (S j0) (\lambda (ee: nat).(match ee in nat
 499 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
 500 True])) I O H2) in (False_ind (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2))
 501 (\lambda (c1: C).(drop i (S j0) c1 (CSort n)))) H5)))))) (drop_gen_sort n (S
 502 j0) O e2 H)))))))) (\lambda (e2: C).(\lambda (IHe1: ((\forall (e3: C).((drop
 503 (S j0) O e2 e3) \to (\forall (c2: C).(\forall (i: nat).((drop i O c2 e3) \to
 504 (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S
 505 j0) c1 e2)))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e3: C).(\lambda
 506 (H: (drop (S j0) O (CHead e2 k t) e3)).(\lambda (c2: C).(\lambda (i:
 507 nat).(\lambda (H0: (drop i O c2 e3)).(K_ind (\lambda (k0: K).((drop (r k0 j0)
 508 O e2 e3) \to (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1:
 509 C).(drop i (S j0) c1 (CHead e2 k0 t)))))) (\lambda (b: B).(\lambda (H1: (drop
 510 (r (Bind b) j0) O e2 e3)).(let H_x \def (IHj e2 e3 H1 c2 i H0) in (let H2
 511 \def H_x in (ex2_ind C (\lambda (c1: C).(drop j0 O c1 c2)) (\lambda (c1:
 512 C).(drop i j0 c1 e2)) (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda
 513 (c1: C).(drop i (S j0) c1 (CHead e2 (Bind b) t)))) (\lambda (x: C).(\lambda
 514 (H3: (drop j0 O x c2)).(\lambda (H4: (drop i j0 x e2)).(ex_intro2 C (\lambda
 515 (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2
 516 (Bind b) t))) (CHead x (Bind b) (lift i (r (Bind b) j0) t)) (drop_drop (Bind
 517 b) j0 x c2 H3 (lift i (r (Bind b) j0) t)) (drop_skip (Bind b) i j0 x e2 H4
 518 t))))) H2))))) (\lambda (f: F).(\lambda (H1: (drop (r (Flat f) j0) O e2
 519 e3)).(let H_x \def (IHe1 e3 H1 c2 i H0) in (let H2 \def H_x in (ex2_ind C
 520 (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1
 521 e2)) (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i
 522 (S j0) c1 (CHead e2 (Flat f) t)))) (\lambda (x: C).(\lambda (H3: (drop (S j0)
 523 O x c2)).(\lambda (H4: (drop i (S j0) x e2)).(ex_intro2 C (\lambda (c1:
 524 C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2 (Flat
 525 f) t))) (CHead x (Flat f) (lift i (r (Flat f) j0) t)) (drop_drop (Flat f) j0
 526 x c2 H3 (lift i (r (Flat f) j0) t)) (drop_skip (Flat f) i j0 x e2 H4 t)))))
 527 H2))))) k (drop_gen_drop k e2 e3 t j0 H))))))))))) e1)))) j).
 528 (* COMMENTS
 529 Initial nodes: 1154
 530 END *)
 531
 532 theorem drop_trans_le:
 533  \forall (i: nat).(\forall (d: nat).((le i d) \to (\forall (c1: C).(\forall
 534 (c2: C).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((drop i O
 535 c2 e2) \to (ex2 C (\lambda (e1: C).(drop i O c1 e1)) (\lambda (e1: C).(drop h
 536 (minus d i) e1 e2)))))))))))
 537 \def
 538  \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (d: nat).((le n d) \to
 539 (\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((drop h d c1 c2) \to
 540 (\forall (e2: C).((drop n O c2 e2) \to (ex2 C (\lambda (e1: C).(drop n O c1
 541 e1)) (\lambda (e1: C).(drop h (minus d n) e1 e2)))))))))))) (\lambda (d:
 542 nat).(\lambda (_: (le O d)).(\lambda (c1: C).(\lambda (c2: C).(\lambda (h:
 543 nat).(\lambda (H0: (drop h d c1 c2)).(\lambda (e2: C).(\lambda (H1: (drop O O
 544 c2 e2)).(let H2 \def (eq_ind C c2 (\lambda (c: C).(drop h d c1 c)) H0 e2
 545 (drop_gen_refl c2 e2 H1)) in (eq_ind nat d (\lambda (n: nat).(ex2 C (\lambda
 546 (e1: C).(drop O O c1 e1)) (\lambda (e1: C).(drop h n e1 e2)))) (ex_intro2 C
 547 (\lambda (e1: C).(drop O O c1 e1)) (\lambda (e1: C).(drop h d e1 e2)) c1
 548 (drop_refl c1) H2) (minus d O) (minus_n_O d))))))))))) (\lambda (i0:
 549 nat).(\lambda (IHi: ((\forall (d: nat).((le i0 d) \to (\forall (c1:
 550 C).(\forall (c2: C).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2:
 551 C).((drop i0 O c2 e2) \to (ex2 C (\lambda (e1: C).(drop i0 O c1 e1)) (\lambda
 552 (e1: C).(drop h (minus d i0) e1 e2))))))))))))).(\lambda (d: nat).(nat_ind
 553 (\lambda (n: nat).((le (S i0) n) \to (\forall (c1: C).(\forall (c2:
 554 C).(\forall (h: nat).((drop h n c1 c2) \to (\forall (e2: C).((drop (S i0) O
 555 c2 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1:
 556 C).(drop h (minus n (S i0)) e1 e2))))))))))) (\lambda (H: (le (S i0)
 557 O)).(\lambda (c1: C).(\lambda (c2: C).(\lambda (h: nat).(\lambda (_: (drop h
 558 O c1 c2)).(\lambda (e2: C).(\lambda (_: (drop (S i0) O c2 e2)).(ex2_ind nat
 559 (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le i0 n)) (ex2 C
 560 (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1: C).(drop h (minus O (S
 561 i0)) e1 e2))) (\lambda (x: nat).(\lambda (H2: (eq nat O (S x))).(\lambda (_:
 562 (le i0 x)).(let H4 \def (eq_ind nat O (\lambda (ee: nat).(match ee in nat
 563 return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow
 564 False])) I (S x) H2) in (False_ind (ex2 C (\lambda (e1: C).(drop (S i0) O c1
 565 e1)) (\lambda (e1: C).(drop h (minus O (S i0)) e1 e2))) H4))))) (le_gen_S i0
 566 O H))))))))) (\lambda (d0: nat).(\lambda (_: (((le (S i0) d0) \to (\forall
 567 (c1: C).(\forall (c2: C).(\forall (h: nat).((drop h d0 c1 c2) \to (\forall
 568 (e2: C).((drop (S i0) O c2 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1
 569 e1)) (\lambda (e1: C).(drop h (minus d0 (S i0)) e1 e2)))))))))))).(\lambda
 570 (H: (le (S i0) (S d0))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2:
 571 C).(\forall (h: nat).((drop h (S d0) c c2) \to (\forall (e2: C).((drop (S i0)
 572 O c2 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c e1)) (\lambda (e1:
 573 C).(drop h (minus (S d0) (S i0)) e1 e2))))))))) (\lambda (n: nat).(\lambda
 574 (c2: C).(\lambda (h: nat).(\lambda (H0: (drop h (S d0) (CSort n)
 575 c2)).(\lambda (e2: C).(\lambda (H1: (drop (S i0) O c2 e2)).(and3_ind (eq C c2
 576 (CSort n)) (eq nat h O) (eq nat (S d0) O) (ex2 C (\lambda (e1: C).(drop (S
 577 i0) O (CSort n) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2)))
 578 (\lambda (H2: (eq C c2 (CSort n))).(\lambda (_: (eq nat h O)).(\lambda (_:
 579 (eq nat (S d0) O)).(let H5 \def (eq_ind C c2 (\lambda (c: C).(drop (S i0) O c
 580 e2)) H1 (CSort n) H2) in (and3_ind (eq C e2 (CSort n)) (eq nat (S i0) O) (eq
 581 nat O O) (ex2 C (\lambda (e1: C).(drop (S i0) O (CSort n) e1)) (\lambda (e1:
 582 C).(drop h (minus (S d0) (S i0)) e1 e2))) (\lambda (H6: (eq C e2 (CSort
 583 n))).(\lambda (H7: (eq nat (S i0) O)).(\lambda (_: (eq nat O O)).(eq_ind_r C
 584 (CSort n) (\lambda (c: C).(ex2 C (\lambda (e1: C).(drop (S i0) O (CSort n)
 585 e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 c)))) (let H9 \def
 586 (eq_ind nat (S i0) (\lambda (ee: nat).(match ee in nat return (\lambda (_:
 587 nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H7) in
 588 (False_ind (ex2 C (\lambda (e1: C).(drop (S i0) O (CSort n) e1)) (\lambda
 589 (e1: C).(drop h (minus (S d0) (S i0)) e1 (CSort n)))) H9)) e2 H6))))
 590 (drop_gen_sort n (S i0) O e2 H5)))))) (drop_gen_sort n h (S d0) c2 H0))))))))
 591 (\lambda (c2: C).(\lambda (IHc: ((\forall (c3: C).(\forall (h: nat).((drop h
 592 (S d0) c2 c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to (ex2 C (\lambda
 593 (e1: C).(drop (S i0) O c2 e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0))
 594 e1 e2)))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t:
 595 T).(\forall (c3: C).(\forall (h: nat).((drop h (S d0) (CHead c2 k0 t) c3) \to
 596 (\forall (e2: C).((drop (S i0) O c3 e2) \to (ex2 C (\lambda (e1: C).(drop (S
 597 i0) O (CHead c2 k0 t) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1
 598 e2)))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (c3: C).(\lambda (h:
 599 nat).(\lambda (H0: (drop h (S d0) (CHead c2 (Bind b) t) c3)).(\lambda (e2:
 600 C).(\lambda (H1: (drop (S i0) O c3 e2)).(ex3_2_ind C T (\lambda (e:
 601 C).(\lambda (v: T).(eq C c3 (CHead e (Bind b) v)))) (\lambda (_: C).(\lambda
 602 (v: T).(eq T t (lift h (r (Bind b) d0) v)))) (\lambda (e: C).(\lambda (_:
 603 T).(drop h (r (Bind b) d0) c2 e))) (ex2 C (\lambda (e1: C).(drop (S i0) O
 604 (CHead c2 (Bind b) t) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1
 605 e2))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H2: (eq C c3 (CHead x0
 606 (Bind b) x1))).(\lambda (H3: (eq T t (lift h (r (Bind b) d0) x1))).(\lambda
 607 (H4: (drop h (r (Bind b) d0) c2 x0)).(let H5 \def (eq_ind C c3 (\lambda (c:
 608 C).(drop (S i0) O c e2)) H1 (CHead x0 (Bind b) x1) H2) in (eq_ind_r T (lift h
 609 (r (Bind b) d0) x1) (\lambda (t0: T).(ex2 C (\lambda (e1: C).(drop (S i0) O
 610 (CHead c2 (Bind b) t0) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1
 611 e2)))) (ex2_ind C (\lambda (e1: C).(drop i0 O c2 e1)) (\lambda (e1: C).(drop
 612 h (minus d0 i0) e1 e2)) (ex2 C (\lambda (e1: C).(drop (S i0) O (CHead c2
 613 (Bind b) (lift h (r (Bind b) d0) x1)) e1)) (\lambda (e1: C).(drop h (minus (S
 614 d0) (S i0)) e1 e2))) (\lambda (x: C).(\lambda (H6: (drop i0 O c2 x)).(\lambda
 615 (H7: (drop h (minus d0 i0) x e2)).(ex_intro2 C (\lambda (e1: C).(drop (S i0)
 616 O (CHead c2 (Bind b) (lift h (r (Bind b) d0) x1)) e1)) (\lambda (e1: C).(drop
 617 h (minus (S d0) (S i0)) e1 e2)) x (drop_drop (Bind b) i0 c2 x H6 (lift h (r
 618 (Bind b) d0) x1)) H7)))) (IHi d0 (le_S_n i0 d0 H) c2 x0 h H4 e2
 619 (drop_gen_drop (Bind b) x0 e2 x1 i0 H5))) t H3))))))) (drop_gen_skip_l c2 c3
 620 t h d0 (Bind b) H0))))))))) (\lambda (f: F).(\lambda (t: T).(\lambda (c3:
 621 C).(\lambda (h: nat).(\lambda (H0: (drop h (S d0) (CHead c2 (Flat f) t)
 622 c3)).(\lambda (e2: C).(\lambda (H1: (drop (S i0) O c3 e2)).(ex3_2_ind C T
 623 (\lambda (e: C).(\lambda (v: T).(eq C c3 (CHead e (Flat f) v)))) (\lambda (_:
 624 C).(\lambda (v: T).(eq T t (lift h (r (Flat f) d0) v)))) (\lambda (e:
 625 C).(\lambda (_: T).(drop h (r (Flat f) d0) c2 e))) (ex2 C (\lambda (e1:
 626 C).(drop (S i0) O (CHead c2 (Flat f) t) e1)) (\lambda (e1: C).(drop h (minus
 627 (S d0) (S i0)) e1 e2))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H2: (eq C
 628 c3 (CHead x0 (Flat f) x1))).(\lambda (H3: (eq T t (lift h (r (Flat f) d0)
 629 x1))).(\lambda (H4: (drop h (r (Flat f) d0) c2 x0)).(let H5 \def (eq_ind C c3
 630 (\lambda (c: C).(drop (S i0) O c e2)) H1 (CHead x0 (Flat f) x1) H2) in
 631 (eq_ind_r T (lift h (r (Flat f) d0) x1) (\lambda (t0: T).(ex2 C (\lambda (e1:
 632 C).(drop (S i0) O (CHead c2 (Flat f) t0) e1)) (\lambda (e1: C).(drop h (minus
 633 (S d0) (S i0)) e1 e2)))) (ex2_ind C (\lambda (e1: C).(drop (S i0) O c2 e1))
 634 (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2)) (ex2 C (\lambda (e1:
 635 C).(drop (S i0) O (CHead c2 (Flat f) (lift h (r (Flat f) d0) x1)) e1))
 636 (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2))) (\lambda (x:
 637 C).(\lambda (H6: (drop (S i0) O c2 x)).(\lambda (H7: (drop h (minus (S d0) (S
 638 i0)) x e2)).(ex_intro2 C (\lambda (e1: C).(drop (S i0) O (CHead c2 (Flat f)
 639 (lift h (r (Flat f) d0) x1)) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S
 640 i0)) e1 e2)) x (drop_drop (Flat f) i0 c2 x H6 (lift h (r (Flat f) d0) x1))
 641 H7)))) (IHc x0 h H4 e2 (drop_gen_drop (Flat f) x0 e2 x1 i0 H5))) t H3)))))))
 642 (drop_gen_skip_l c2 c3 t h d0 (Flat f) H0))))))))) k)))) c1))))) d)))) i).
 643 (* COMMENTS
 644 Initial nodes: 2453
 645 END *)
 646
 647 theorem drop_trans_ge:
 648  \forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (d:
 649 nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((drop i O c2
 650 e2) \to ((le d i) \to (drop (plus i h) O c1 e2)))))))))
 651 \def
 652  \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (c2:
 653 C).(\forall (d: nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2:
 654 C).((drop n O c2 e2) \to ((le d n) \to (drop (plus n h) O c1 e2))))))))))
 655 (\lambda (c1: C).(\lambda (c2: C).(\lambda (d: nat).(\lambda (h:
 656 nat).(\lambda (H: (drop h d c1 c2)).(\lambda (e2: C).(\lambda (H0: (drop O O
 657 c2 e2)).(\lambda (H1: (le d O)).(eq_ind C c2 (\lambda (c: C).(drop (plus O h)
 658 O c1 c)) (let H_y \def (le_n_O_eq d H1) in (let H2 \def (eq_ind_r nat d
 659 (\lambda (n: nat).(drop h n c1 c2)) H O H_y) in H2)) e2 (drop_gen_refl c2 e2
 660 H0)))))))))) (\lambda (i0: nat).(\lambda (IHi: ((\forall (c1: C).(\forall
 661 (c2: C).(\forall (d: nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall
 662 (e2: C).((drop i0 O c2 e2) \to ((le d i0) \to (drop (plus i0 h) O c1
 663 e2))))))))))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2:
 664 C).(\forall (d: nat).(\forall (h: nat).((drop h d c c2) \to (\forall (e2:
 665 C).((drop (S i0) O c2 e2) \to ((le d (S i0)) \to (drop (plus (S i0) h) O c
 666 e2))))))))) (\lambda (n: nat).(\lambda (c2: C).(\lambda (d: nat).(\lambda (h:
 667 nat).(\lambda (H: (drop h d (CSort n) c2)).(\lambda (e2: C).(\lambda (H0:
 668 (drop (S i0) O c2 e2)).(\lambda (H1: (le d (S i0))).(and3_ind (eq C c2 (CSort
 669 n)) (eq nat h O) (eq nat d O) (drop (S (plus i0 h)) O (CSort n) e2) (\lambda
 670 (H2: (eq C c2 (CSort n))).(\lambda (H3: (eq nat h O)).(\lambda (H4: (eq nat d
 671 O)).(eq_ind_r nat O (\lambda (n0: nat).(drop (S (plus i0 n0)) O (CSort n)
 672 e2)) (let H5 \def (eq_ind nat d (\lambda (n0: nat).(le n0 (S i0))) H1 O H4)
 673 in (let H6 \def (eq_ind C c2 (\lambda (c: C).(drop (S i0) O c e2)) H0 (CSort
 674 n) H2) in (and3_ind (eq C e2 (CSort n)) (eq nat (S i0) O) (eq nat O O) (drop
 675 (S (plus i0 O)) O (CSort n) e2) (\lambda (H7: (eq C e2 (CSort n))).(\lambda
 676 (H8: (eq nat (S i0) O)).(\lambda (_: (eq nat O O)).(eq_ind_r C (CSort n)
 677 (\lambda (c: C).(drop (S (plus i0 O)) O (CSort n) c)) (let H10 \def (eq_ind
 678 nat (S i0) (\lambda (ee: nat).(match ee in nat return (\lambda (_: nat).Prop)
 679 with [O \Rightarrow False | (S _) \Rightarrow True])) I O H8) in (False_ind
 680 (drop (S (plus i0 O)) O (CSort n) (CSort n)) H10)) e2 H7)))) (drop_gen_sort n
 681 (S i0) O e2 H6)))) h H3)))) (drop_gen_sort n h d c2 H)))))))))) (\lambda (c2:
 682 C).(\lambda (IHc: ((\forall (c3: C).(\forall (d: nat).(\forall (h:
 683 nat).((drop h d c2 c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to ((le d
 684 (S i0)) \to (drop (S (plus i0 h)) O c2 e2)))))))))).(\lambda (k: K).(\lambda
 685 (t: T).(\lambda (c3: C).(\lambda (d: nat).(nat_ind (\lambda (n: nat).(\forall
 686 (h: nat).((drop h n (CHead c2 k t) c3) \to (\forall (e2: C).((drop (S i0) O
 687 c3 e2) \to ((le n (S i0)) \to (drop (S (plus i0 h)) O (CHead c2 k t)
 688 e2))))))) (\lambda (h: nat).(nat_ind (\lambda (n: nat).((drop n O (CHead c2 k
 689 t) c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to ((le O (S i0)) \to
 690 (drop (S (plus i0 n)) O (CHead c2 k t) e2)))))) (\lambda (H: (drop O O (CHead
 691 c2 k t) c3)).(\lambda (e2: C).(\lambda (H0: (drop (S i0) O c3 e2)).(\lambda
 692 (_: (le O (S i0))).(let H2 \def (eq_ind_r C c3 (\lambda (c: C).(drop (S i0) O
 693 c e2)) H0 (CHead c2 k t) (drop_gen_refl (CHead c2 k t) c3 H)) in (eq_ind nat
 694 i0 (\lambda (n: nat).(drop (S n) O (CHead c2 k t) e2)) (drop_drop k i0 c2 e2
 695 (drop_gen_drop k c2 e2 t i0 H2) t) (plus i0 O) (plus_n_O i0))))))) (\lambda
 696 (n: nat).(\lambda (_: (((drop n O (CHead c2 k t) c3) \to (\forall (e2:
 697 C).((drop (S i0) O c3 e2) \to ((le O (S i0)) \to (drop (S (plus i0 n)) O
 698 (CHead c2 k t) e2))))))).(\lambda (H0: (drop (S n) O (CHead c2 k t)
 699 c3)).(\lambda (e2: C).(\lambda (H1: (drop (S i0) O c3 e2)).(\lambda (H2: (le
 700 O (S i0))).(eq_ind nat (S (plus i0 n)) (\lambda (n0: nat).(drop (S n0) O
 701 (CHead c2 k t) e2)) (drop_drop k (S (plus i0 n)) c2 e2 (eq_ind_r nat (S (r k
 702 (plus i0 n))) (\lambda (n0: nat).(drop n0 O c2 e2)) (eq_ind_r nat (plus i0 (r
 703 k n)) (\lambda (n0: nat).(drop (S n0) O c2 e2)) (IHc c3 O (r k n)
 704 (drop_gen_drop k c2 c3 t n H0) e2 H1 H2) (r k (plus i0 n)) (r_plus_sym k i0
 705 n)) (r k (S (plus i0 n))) (r_S k (plus i0 n))) t) (plus i0 (S n)) (plus_n_Sm
 706 i0 n)))))))) h)) (\lambda (d0: nat).(\lambda (IHd: ((\forall (h: nat).((drop
 707 h d0 (CHead c2 k t) c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to ((le
 708 d0 (S i0)) \to (drop (S (plus i0 h)) O (CHead c2 k t) e2)))))))).(\lambda (h:
 709 nat).(\lambda (H: (drop h (S d0) (CHead c2 k t) c3)).(\lambda (e2:
 710 C).(\lambda (H0: (drop (S i0) O c3 e2)).(\lambda (H1: (le (S d0) (S
 711 i0))).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C c3 (CHead e k
 712 v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k d0) v)))) (\lambda
 713 (e: C).(\lambda (_: T).(drop h (r k d0) c2 e))) (drop (S (plus i0 h)) O
 714 (CHead c2 k t) e2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H2: (eq C c3
 715 (CHead x0 k x1))).(\lambda (H3: (eq T t (lift h (r k d0) x1))).(\lambda (H4:
 716 (drop h (r k d0) c2 x0)).(let H5 \def (eq_ind C c3 (\lambda (c: C).(\forall
 717 (h0: nat).((drop h0 d0 (CHead c2 k t) c) \to (\forall (e3: C).((drop (S i0) O
 718 c e3) \to ((le d0 (S i0)) \to (drop (S (plus i0 h0)) O (CHead c2 k t)
 719 e3))))))) IHd (CHead x0 k x1) H2) in (let H6 \def (eq_ind C c3 (\lambda (c:
 720 C).(drop (S i0) O c e2)) H0 (CHead x0 k x1) H2) in (let H7 \def (eq_ind T t
 721 (\lambda (t0: T).(\forall (h0: nat).((drop h0 d0 (CHead c2 k t0) (CHead x0 k
 722 x1)) \to (\forall (e3: C).((drop (S i0) O (CHead x0 k x1) e3) \to ((le d0 (S
 723 i0)) \to (drop (S (plus i0 h0)) O (CHead c2 k t0) e3))))))) H5 (lift h (r k
 724 d0) x1) H3) in (eq_ind_r T (lift h (r k d0) x1) (\lambda (t0: T).(drop (S
 725 (plus i0 h)) O (CHead c2 k t0) e2)) (drop_drop k (plus i0 h) c2 e2 (K_ind
 726 (\lambda (k0: K).((drop h (r k0 d0) c2 x0) \to ((drop (r k0 i0) O x0 e2) \to
 727 (drop (r k0 (plus i0 h)) O c2 e2)))) (\lambda (b: B).(\lambda (H8: (drop h (r
 728 (Bind b) d0) c2 x0)).(\lambda (H9: (drop (r (Bind b) i0) O x0 e2)).(IHi c2 x0
 729 (r (Bind b) d0) h H8 e2 H9 (le_S_n (r (Bind b) d0) i0 H1))))) (\lambda (f:
 730 F).(\lambda (H8: (drop h (r (Flat f) d0) c2 x0)).(\lambda (H9: (drop (r (Flat
 731 f) i0) O x0 e2)).(IHc x0 (r (Flat f) d0) h H8 e2 H9 H1)))) k H4
 732 (drop_gen_drop k x0 e2 x1 i0 H6)) (lift h (r k d0) x1)) t H3)))))))))
 733 (drop_gen_skip_l c2 c3 t h d0 k H))))))))) d))))))) c1)))) i).
 734 (* COMMENTS
 735 Initial nodes: 2020
 736 END *)
 737