matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/fwd.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 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/drop/fwd".
  18
  19 include "drop/defs.ma".
  20
  21 theorem drop_gen_sort:
  22  \forall (n: nat).(\forall (h: nat).(\forall (d: nat).(\forall (x: C).((drop
  23 h d (CSort n) x) \to (and3 (eq C x (CSort n)) (eq nat h O) (eq nat d O))))))
  24 \def
  25  \lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (x:
  26 C).(\lambda (H: (drop h d (CSort n) x)).(insert_eq C (CSort n) (\lambda (c:
  27 C).(drop h d c x)) (and3 (eq C x (CSort n)) (eq nat h O) (eq nat d O))
  28 (\lambda (y: C).(\lambda (H0: (drop h d y x)).(drop_ind (\lambda (n0:
  29 nat).(\lambda (n1: nat).(\lambda (c: C).(\lambda (c0: C).((eq C c (CSort n))
  30 \to (and3 (eq C c0 (CSort n)) (eq nat n0 O) (eq nat n1 O))))))) (\lambda (c:
  31 C).(\lambda (H1: (eq C c (CSort n))).(let H2 \def (f_equal C C (\lambda (e:
  32 C).e) c (CSort n) H1) in (eq_ind_r C (CSort n) (\lambda (c0: C).(and3 (eq C
  33 c0 (CSort n)) (eq nat O O) (eq nat O O))) (and3_intro (eq C (CSort n) (CSort
  34 n)) (eq nat O O) (eq nat O O) (refl_equal C (CSort n)) (refl_equal nat O)
  35 (refl_equal nat O)) c H2)))) (\lambda (k: K).(\lambda (h0: nat).(\lambda (c:
  36 C).(\lambda (e: C).(\lambda (_: (drop (r k h0) O c e)).(\lambda (_: (((eq C c
  37 (CSort n)) \to (and3 (eq C e (CSort n)) (eq nat (r k h0) O) (eq nat O
  38 O))))).(\lambda (u: T).(\lambda (H3: (eq C (CHead c k u) (CSort n))).(let H4
  39 \def (eq_ind C (CHead c k u) (\lambda (ee: C).(match ee in C return (\lambda
  40 (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow
  41 True])) I (CSort n) H3) in (False_ind (and3 (eq C e (CSort n)) (eq nat (S h0)
  42 O) (eq nat O O)) H4)))))))))) (\lambda (k: K).(\lambda (h0: nat).(\lambda
  43 (d0: nat).(\lambda (c: C).(\lambda (e: C).(\lambda (_: (drop h0 (r k d0) c
  44 e)).(\lambda (_: (((eq C c (CSort n)) \to (and3 (eq C e (CSort n)) (eq nat h0
  45 O) (eq nat (r k d0) O))))).(\lambda (u: T).(\lambda (H3: (eq C (CHead c k
  46 (lift h0 (r k d0) u)) (CSort n))).(let H4 \def (eq_ind C (CHead c k (lift h0
  47 (r k d0) u)) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop)
  48 with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I
  49 (CSort n) H3) in (False_ind (and3 (eq C (CHead e k u) (CSort n)) (eq nat h0
  50 O) (eq nat (S d0) O)) H4))))))))))) h d y x H0))) H))))).
  51
  52 theorem drop_gen_refl:
  53  \forall (x: C).(\forall (e: C).((drop O O x e) \to (eq C x e)))
  54 \def
  55  \lambda (x: C).(\lambda (e: C).(\lambda (H: (drop O O x e)).(insert_eq nat O
  56 (\lambda (n: nat).(drop n O x e)) (eq C x e) (\lambda (y: nat).(\lambda (H0:
  57 (drop y O x e)).(insert_eq nat O (\lambda (n: nat).(drop y n x e)) ((eq nat y
  58 O) \to (eq C x e)) (\lambda (y0: nat).(\lambda (H1: (drop y y0 x
  59 e)).(drop_ind (\lambda (n: nat).(\lambda (n0: nat).(\lambda (c: C).(\lambda
  60 (c0: C).((eq nat n0 O) \to ((eq nat n O) \to (eq C c c0))))))) (\lambda (c:
  61 C).(\lambda (_: (eq nat O O)).(\lambda (_: (eq nat O O)).(refl_equal C c))))
  62 (\lambda (k: K).(\lambda (h: nat).(\lambda (c: C).(\lambda (e0: C).(\lambda
  63 (_: (drop (r k h) O c e0)).(\lambda (_: (((eq nat O O) \to ((eq nat (r k h)
  64 O) \to (eq C c e0))))).(\lambda (u: T).(\lambda (_: (eq nat O O)).(\lambda
  65 (H5: (eq nat (S h) O)).(let H6 \def (eq_ind nat (S h) (\lambda (ee:
  66 nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
  67 False | (S _) \Rightarrow True])) I O H5) in (False_ind (eq C (CHead c k u)
  68 e0) H6))))))))))) (\lambda (k: K).(\lambda (h: nat).(\lambda (d:
  69 nat).(\lambda (c: C).(\lambda (e0: C).(\lambda (H2: (drop h (r k d) c
  70 e0)).(\lambda (H3: (((eq nat (r k d) O) \to ((eq nat h O) \to (eq C c
  71 e0))))).(\lambda (u: T).(\lambda (H4: (eq nat (S d) O)).(\lambda (H5: (eq nat
  72 h O)).(let H6 \def (f_equal nat nat (\lambda (e1: nat).e1) h O H5) in (let H7
  73 \def (eq_ind nat h (\lambda (n: nat).((eq nat (r k d) O) \to ((eq nat n O)
  74 \to (eq C c e0)))) H3 O H6) in (let H8 \def (eq_ind nat h (\lambda (n:
  75 nat).(drop n (r k d) c e0)) H2 O H6) in (eq_ind_r nat O (\lambda (n: nat).(eq
  76 C (CHead c k (lift n (r k d) u)) (CHead e0 k u))) (let H9 \def (eq_ind nat (S
  77 d) (\lambda (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O
  78 \Rightarrow False | (S _) \Rightarrow True])) I O H4) in (False_ind (eq C
  79 (CHead c k (lift O (r k d) u)) (CHead e0 k u)) H9)) h H6)))))))))))))) y y0 x
  80 e H1))) H0))) H))).
  81
  82 theorem drop_gen_drop:
  83  \forall (k: K).(\forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h:
  84 nat).((drop (S h) O (CHead c k u) x) \to (drop (r k h) O c x))))))
  85 \def
  86  \lambda (k: K).(\lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h:
  87 nat).(\lambda (H: (drop (S h) O (CHead c k u) x)).(insert_eq C (CHead c k u)
  88 (\lambda (c0: C).(drop (S h) O c0 x)) (drop (r k h) O c x) (\lambda (y:
  89 C).(\lambda (H0: (drop (S h) O y x)).(insert_eq nat O (\lambda (n: nat).(drop
  90 (S h) n y x)) ((eq C y (CHead c k u)) \to (drop (r k h) O c x)) (\lambda (y0:
  91 nat).(\lambda (H1: (drop (S h) y0 y x)).(insert_eq nat (S h) (\lambda (n:
  92 nat).(drop n y0 y x)) ((eq nat y0 O) \to ((eq C y (CHead c k u)) \to (drop (r
  93 k h) O c x))) (\lambda (y1: nat).(\lambda (H2: (drop y1 y0 y x)).(drop_ind
  94 (\lambda (n: nat).(\lambda (n0: nat).(\lambda (c0: C).(\lambda (c1: C).((eq
  95 nat n (S h)) \to ((eq nat n0 O) \to ((eq C c0 (CHead c k u)) \to (drop (r k
  96 h) O c c1)))))))) (\lambda (c0: C).(\lambda (H3: (eq nat O (S h))).(\lambda
  97 (_: (eq nat O O)).(\lambda (_: (eq C c0 (CHead c k u))).(let H6 \def (match
  98 H3 in eq return (\lambda (n: nat).(\lambda (_: (eq ? ? n)).((eq nat n (S h))
  99 \to (drop (r k h) O c c0)))) with [refl_equal \Rightarrow (\lambda (H2: (eq
 100 nat O (S h))).(let H3 \def (eq_ind nat O (\lambda (e: nat).(match e in nat
 101 return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow
 102 False])) I (S h) H2) in (False_ind (drop (r k h) O c c0) H3)))]) in (H6
 103 (refl_equal nat (S h)))))))) (\lambda (k0: K).(\lambda (h0: nat).(\lambda
 104 (c0: C).(\lambda (e: C).(\lambda (H3: (drop (r k0 h0) O c0 e)).(\lambda (_:
 105 (((eq nat (r k0 h0) (S h)) \to ((eq nat O O) \to ((eq C c0 (CHead c k u)) \to
 106 (drop (r k h) O c e)))))).(\lambda (u0: T).(\lambda (H5: (eq nat (S h0) (S
 107 h))).(\lambda (_: (eq nat O O)).(\lambda (H7: (eq C (CHead c0 k0 u0) (CHead c
 108 k u))).(let H8 \def (match H5 in eq return (\lambda (n: nat).(\lambda (_: (eq
 109 ? ? n)).((eq nat n (S h)) \to (drop (r k h) O c e)))) with [refl_equal
 110 \Rightarrow (\lambda (H4: (eq nat (S h0) (S h))).(let H5 \def (f_equal nat
 111 nat (\lambda (e0: nat).(match e0 in nat return (\lambda (_: nat).nat) with [O
 112 \Rightarrow h0 | (S n) \Rightarrow n])) (S h0) (S h) H4) in (eq_ind nat h
 113 (\lambda (_: nat).(drop (r k h) O c e)) (let H6 \def (match H7 in eq return
 114 (\lambda (c0: C).(\lambda (_: (eq ? ? c0)).((eq C c0 (CHead c k u)) \to (drop
 115 (r k h) O c e)))) with [refl_equal \Rightarrow (\lambda (H4: (eq C (CHead c0
 116 k0 u0) (CHead c k u))).(let H6 \def (f_equal C T (\lambda (e0: C).(match e0
 117 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t)
 118 \Rightarrow t])) (CHead c0 k0 u0) (CHead c k u) H4) in ((let H7 \def (f_equal
 119 C K (\lambda (e0: C).(match e0 in C return (\lambda (_: C).K) with [(CSort _)
 120 \Rightarrow k0 | (CHead _ k _) \Rightarrow k])) (CHead c0 k0 u0) (CHead c k
 121 u) H4) in ((let H8 \def (f_equal C C (\lambda (e0: C).(match e0 in C return
 122 (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow
 123 c])) (CHead c0 k0 u0) (CHead c k u) H4) in (eq_ind C c (\lambda (_: C).((eq K
 124 k0 k) \to ((eq T u0 u) \to (drop (r k h) O c e)))) (\lambda (H9: (eq K k0
 125 k)).(eq_ind K k (\lambda (_: K).((eq T u0 u) \to (drop (r k h) O c e)))
 126 (\lambda (H10: (eq T u0 u)).(eq_ind T u (\lambda (_: T).(drop (r k h) O c e))
 127 (eq_ind nat h0 (\lambda (n: nat).(drop (r k n) O c e)) (eq_ind C c0 (\lambda
 128 (c: C).(drop (r k h0) O c e)) (eq_ind K k0 (\lambda (k: K).(drop (r k h0) O
 129 c0 e)) H3 k H9) c H8) h H5) u0 (sym_eq T u0 u H10))) k0 (sym_eq K k0 k H9)))
 130 c0 (sym_eq C c0 c H8))) H7)) H6)))]) in (H6 (refl_equal C (CHead c k u)))) h0
 131 (sym_eq nat h0 h H5))))]) in (H8 (refl_equal nat (S h)))))))))))))) (\lambda
 132 (k0: K).(\lambda (h0: nat).(\lambda (d: nat).(\lambda (c0: C).(\lambda (e:
 133 C).(\lambda (_: (drop h0 (r k0 d) c0 e)).(\lambda (_: (((eq nat h0 (S h)) \to
 134 ((eq nat (r k0 d) O) \to ((eq C c0 (CHead c k u)) \to (drop (r k h) O c
 135 e)))))).(\lambda (u0: T).(\lambda (_: (eq nat h0 (S h))).(\lambda (H6: (eq
 136 nat (S d) O)).(\lambda (_: (eq C (CHead c0 k0 (lift h0 (r k0 d) u0)) (CHead c
 137 k u))).(let H8 \def (match H6 in eq return (\lambda (n: nat).(\lambda (_: (eq
 138 ? ? n)).((eq nat n O) \to (drop (r k h) O c (CHead e k0 u0))))) with
 139 [refl_equal \Rightarrow (\lambda (H4: (eq nat (S d) O)).(let H5 \def (eq_ind
 140 nat (S d) (\lambda (e0: nat).(match e0 in nat return (\lambda (_: nat).Prop)
 141 with [O \Rightarrow False | (S _) \Rightarrow True])) I O H4) in (False_ind
 142 (drop (r k h) O c (CHead e k0 u0)) H5)))]) in (H8 (refl_equal nat
 143 O)))))))))))))) y1 y0 y x H2))) H1))) H0))) H)))))).
 144
 145 theorem drop_gen_skip_r:
 146  \forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: nat).(\forall
 147 (d: nat).(\forall (k: K).((drop h (S d) x (CHead c k u)) \to (ex2 C (\lambda
 148 (e: C).(eq C x (CHead e k (lift h (r k d) u)))) (\lambda (e: C).(drop h (r k
 149 d) e c)))))))))
 150 \def
 151  \lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h: nat).(\lambda
 152 (d: nat).(\lambda (k: K).(\lambda (H: (drop h (S d) x (CHead c k u))).(let H0
 153 \def (match H in drop return (\lambda (n: nat).(\lambda (n0: nat).(\lambda
 154 (c0: C).(\lambda (c1: C).(\lambda (_: (drop n n0 c0 c1)).((eq nat n h) \to
 155 ((eq nat n0 (S d)) \to ((eq C c0 x) \to ((eq C c1 (CHead c k u)) \to (ex2 C
 156 (\lambda (e: C).(eq C x (CHead e k (lift h (r k d) u)))) (\lambda (e:
 157 C).(drop h (r k d) e c)))))))))))) with [(drop_refl c0) \Rightarrow (\lambda
 158 (H0: (eq nat O h)).(\lambda (H1: (eq nat O (S d))).(\lambda (H2: (eq C c0
 159 x)).(\lambda (H3: (eq C c0 (CHead c k u))).(eq_ind nat O (\lambda (n:
 160 nat).((eq nat O (S d)) \to ((eq C c0 x) \to ((eq C c0 (CHead c k u)) \to (ex2
 161 C (\lambda (e: C).(eq C x (CHead e k (lift n (r k d) u)))) (\lambda (e:
 162 C).(drop n (r k d) e c))))))) (\lambda (H4: (eq nat O (S d))).(let H5 \def
 163 (eq_ind nat O (\lambda (e: nat).(match e in nat return (\lambda (_:
 164 nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) I (S d) H4)
 165 in (False_ind ((eq C c0 x) \to ((eq C c0 (CHead c k u)) \to (ex2 C (\lambda
 166 (e: C).(eq C x (CHead e k (lift O (r k d) u)))) (\lambda (e: C).(drop O (r k
 167 d) e c))))) H5))) h H0 H1 H2 H3))))) | (drop_drop k0 h0 c0 e H0 u0)
 168 \Rightarrow (\lambda (H1: (eq nat (S h0) h)).(\lambda (H2: (eq nat O (S
 169 d))).(\lambda (H3: (eq C (CHead c0 k0 u0) x)).(\lambda (H4: (eq C e (CHead c
 170 k u))).(eq_ind nat (S h0) (\lambda (n: nat).((eq nat O (S d)) \to ((eq C
 171 (CHead c0 k0 u0) x) \to ((eq C e (CHead c k u)) \to ((drop (r k0 h0) O c0 e)
 172 \to (ex2 C (\lambda (e0: C).(eq C x (CHead e0 k (lift n (r k d) u))))
 173 (\lambda (e0: C).(drop n (r k d) e0 c)))))))) (\lambda (H5: (eq nat O (S
 174 d))).(let H6 \def (eq_ind nat O (\lambda (e0: nat).(match e0 in nat return
 175 (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False]))
 176 I (S d) H5) in (False_ind ((eq C (CHead c0 k0 u0) x) \to ((eq C e (CHead c k
 177 u)) \to ((drop (r k0 h0) O c0 e) \to (ex2 C (\lambda (e0: C).(eq C x (CHead
 178 e0 k (lift (S h0) (r k d) u)))) (\lambda (e0: C).(drop (S h0) (r k d) e0
 179 c)))))) H6))) h H1 H2 H3 H4 H0))))) | (drop_skip k0 h0 d0 c0 e H0 u0)
 180 \Rightarrow (\lambda (H1: (eq nat h0 h)).(\lambda (H2: (eq nat (S d0) (S
 181 d))).(\lambda (H3: (eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) x)).(\lambda
 182 (H4: (eq C (CHead e k0 u0) (CHead c k u))).(eq_ind nat h (\lambda (n:
 183 nat).((eq nat (S d0) (S d)) \to ((eq C (CHead c0 k0 (lift n (r k0 d0) u0)) x)
 184 \to ((eq C (CHead e k0 u0) (CHead c k u)) \to ((drop n (r k0 d0) c0 e) \to
 185 (ex2 C (\lambda (e0: C).(eq C x (CHead e0 k (lift h (r k d) u)))) (\lambda
 186 (e0: C).(drop h (r k d) e0 c)))))))) (\lambda (H5: (eq nat (S d0) (S
 187 d))).(let H6 \def (f_equal nat nat (\lambda (e0: nat).(match e0 in nat return
 188 (\lambda (_: nat).nat) with [O \Rightarrow d0 | (S n) \Rightarrow n])) (S d0)
 189 (S d) H5) in (eq_ind nat d (\lambda (n: nat).((eq C (CHead c0 k0 (lift h (r
 190 k0 n) u0)) x) \to ((eq C (CHead e k0 u0) (CHead c k u)) \to ((drop h (r k0 n)
 191 c0 e) \to (ex2 C (\lambda (e0: C).(eq C x (CHead e0 k (lift h (r k d) u))))
 192 (\lambda (e0: C).(drop h (r k d) e0 c))))))) (\lambda (H7: (eq C (CHead c0 k0
 193 (lift h (r k0 d) u0)) x)).(eq_ind C (CHead c0 k0 (lift h (r k0 d) u0))
 194 (\lambda (c1: C).((eq C (CHead e k0 u0) (CHead c k u)) \to ((drop h (r k0 d)
 195 c0 e) \to (ex2 C (\lambda (e0: C).(eq C c1 (CHead e0 k (lift h (r k d) u))))
 196 (\lambda (e0: C).(drop h (r k d) e0 c)))))) (\lambda (H8: (eq C (CHead e k0
 197 u0) (CHead c k u))).(let H9 \def (f_equal C T (\lambda (e0: C).(match e0 in C
 198 return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t)
 199 \Rightarrow t])) (CHead e k0 u0) (CHead c k u) H8) in ((let H10 \def (f_equal
 200 C K (\lambda (e0: C).(match e0 in C return (\lambda (_: C).K) with [(CSort _)
 201 \Rightarrow k0 | (CHead _ k _) \Rightarrow k])) (CHead e k0 u0) (CHead c k u)
 202 H8) in ((let H11 \def (f_equal C C (\lambda (e0: C).(match e0 in C return
 203 (\lambda (_: C).C) with [(CSort _) \Rightarrow e | (CHead c _ _) \Rightarrow
 204 c])) (CHead e k0 u0) (CHead c k u) H8) in (eq_ind C c (\lambda (c1: C).((eq K
 205 k0 k) \to ((eq T u0 u) \to ((drop h (r k0 d) c0 c1) \to (ex2 C (\lambda (e0:
 206 C).(eq C (CHead c0 k0 (lift h (r k0 d) u0)) (CHead e0 k (lift h (r k d) u))))
 207 (\lambda (e0: C).(drop h (r k d) e0 c))))))) (\lambda (H12: (eq K k0
 208 k)).(eq_ind K k (\lambda (k1: K).((eq T u0 u) \to ((drop h (r k1 d) c0 c) \to
 209 (ex2 C (\lambda (e0: C).(eq C (CHead c0 k1 (lift h (r k1 d) u0)) (CHead e0 k
 210 (lift h (r k d) u)))) (\lambda (e0: C).(drop h (r k d) e0 c)))))) (\lambda
 211 (H13: (eq T u0 u)).(eq_ind T u (\lambda (t: T).((drop h (r k d) c0 c) \to
 212 (ex2 C (\lambda (e0: C).(eq C (CHead c0 k (lift h (r k d) t)) (CHead e0 k
 213 (lift h (r k d) u)))) (\lambda (e0: C).(drop h (r k d) e0 c))))) (\lambda
 214 (H14: (drop h (r k d) c0 c)).(let H15 \def (eq_ind T u0 (\lambda (t: T).(eq C
 215 (CHead c0 k0 (lift h (r k0 d) t)) x)) H7 u H13) in (let H16 \def (eq_ind K k0
 216 (\lambda (k: K).(eq C (CHead c0 k (lift h (r k d) u)) x)) H15 k H12) in (let
 217 H17 \def (eq_ind_r C x (\lambda (c0: C).(drop h (S d) c0 (CHead c k u))) H
 218 (CHead c0 k (lift h (r k d) u)) H16) in (ex_intro2 C (\lambda (e0: C).(eq C
 219 (CHead c0 k (lift h (r k d) u)) (CHead e0 k (lift h (r k d) u)))) (\lambda
 220 (e0: C).(drop h (r k d) e0 c)) c0 (refl_equal C (CHead c0 k (lift h (r k d)
 221 u))) H14))))) u0 (sym_eq T u0 u H13))) k0 (sym_eq K k0 k H12))) e (sym_eq C e
 222 c H11))) H10)) H9))) x H7)) d0 (sym_eq nat d0 d H6)))) h0 (sym_eq nat h0 h
 223 H1) H2 H3 H4 H0)))))]) in (H0 (refl_equal nat h) (refl_equal nat (S d))
 224 (refl_equal C x) (refl_equal C (CHead c k u)))))))))).
 225
 226 theorem drop_gen_skip_l:
 227  \forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: nat).(\forall
 228 (d: nat).(\forall (k: K).((drop h (S d) (CHead c k u) x) \to (ex3_2 C T
 229 (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda (_:
 230 C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e: C).(\lambda (_:
 231 T).(drop h (r k d) c e))))))))))
 232 \def
 233  \lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h: nat).(\lambda
 234 (d: nat).(\lambda (k: K).(\lambda (H: (drop h (S d) (CHead c k u) x)).(let H0
 235 \def (match H in drop return (\lambda (n: nat).(\lambda (n0: nat).(\lambda
 236 (c0: C).(\lambda (c1: C).(\lambda (_: (drop n n0 c0 c1)).((eq nat n h) \to
 237 ((eq nat n0 (S d)) \to ((eq C c0 (CHead c k u)) \to ((eq C c1 x) \to (ex3_2 C
 238 T (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda (_:
 239 C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e: C).(\lambda (_:
 240 T).(drop h (r k d) c e))))))))))))) with [(drop_refl c0) \Rightarrow (\lambda
 241 (H0: (eq nat O h)).(\lambda (H1: (eq nat O (S d))).(\lambda (H2: (eq C c0
 242 (CHead c k u))).(\lambda (H3: (eq C c0 x)).(eq_ind nat O (\lambda (n:
 243 nat).((eq nat O (S d)) \to ((eq C c0 (CHead c k u)) \to ((eq C c0 x) \to
 244 (ex3_2 C T (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda
 245 (_: C).(\lambda (v: T).(eq T u (lift n (r k d) v)))) (\lambda (e: C).(\lambda
 246 (_: T).(drop n (r k d) c e)))))))) (\lambda (H4: (eq nat O (S d))).(let H5
 247 \def (eq_ind nat O (\lambda (e: nat).(match e in nat return (\lambda (_:
 248 nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) I (S d) H4)
 249 in (False_ind ((eq C c0 (CHead c k u)) \to ((eq C c0 x) \to (ex3_2 C T
 250 (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda (_:
 251 C).(\lambda (v: T).(eq T u (lift O (r k d) v)))) (\lambda (e: C).(\lambda (_:
 252 T).(drop O (r k d) c e)))))) H5))) h H0 H1 H2 H3))))) | (drop_drop k0 h0 c0 e
 253 H0 u0) \Rightarrow (\lambda (H1: (eq nat (S h0) h)).(\lambda (H2: (eq nat O
 254 (S d))).(\lambda (H3: (eq C (CHead c0 k0 u0) (CHead c k u))).(\lambda (H4:
 255 (eq C e x)).(eq_ind nat (S h0) (\lambda (n: nat).((eq nat O (S d)) \to ((eq C
 256 (CHead c0 k0 u0) (CHead c k u)) \to ((eq C e x) \to ((drop (r k0 h0) O c0 e)
 257 \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v))))
 258 (\lambda (_: C).(\lambda (v: T).(eq T u (lift n (r k d) v)))) (\lambda (e0:
 259 C).(\lambda (_: T).(drop n (r k d) c e0))))))))) (\lambda (H5: (eq nat O (S
 260 d))).(let H6 \def (eq_ind nat O (\lambda (e0: nat).(match e0 in nat return
 261 (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False]))
 262 I (S d) H5) in (False_ind ((eq C (CHead c0 k0 u0) (CHead c k u)) \to ((eq C e
 263 x) \to ((drop (r k0 h0) O c0 e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v:
 264 T).(eq C x (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift (S
 265 h0) (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop (S h0) (r k d) c
 266 e0))))))) H6))) h H1 H2 H3 H4 H0))))) | (drop_skip k0 h0 d0 c0 e H0 u0)
 267 \Rightarrow (\lambda (H1: (eq nat h0 h)).(\lambda (H2: (eq nat (S d0) (S
 268 d))).(\lambda (H3: (eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead c k
 269 u))).(\lambda (H4: (eq C (CHead e k0 u0) x)).(eq_ind nat h (\lambda (n:
 270 nat).((eq nat (S d0) (S d)) \to ((eq C (CHead c0 k0 (lift n (r k0 d0) u0))
 271 (CHead c k u)) \to ((eq C (CHead e k0 u0) x) \to ((drop n (r k0 d0) c0 e) \to
 272 (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v))))
 273 (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e0:
 274 C).(\lambda (_: T).(drop h (r k d) c e0))))))))) (\lambda (H5: (eq nat (S d0)
 275 (S d))).(let H6 \def (f_equal nat nat (\lambda (e0: nat).(match e0 in nat
 276 return (\lambda (_: nat).nat) with [O \Rightarrow d0 | (S n) \Rightarrow n]))
 277 (S d0) (S d) H5) in (eq_ind nat d (\lambda (n: nat).((eq C (CHead c0 k0 (lift
 278 h (r k0 n) u0)) (CHead c k u)) \to ((eq C (CHead e k0 u0) x) \to ((drop h (r
 279 k0 n) c0 e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0
 280 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k d) v))))
 281 (\lambda (e0: C).(\lambda (_: T).(drop h (r k d) c e0)))))))) (\lambda (H7:
 282 (eq C (CHead c0 k0 (lift h (r k0 d) u0)) (CHead c k u))).(let H8 \def
 283 (f_equal C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) with
 284 [(CSort _) \Rightarrow ((let rec lref_map (f: ((nat \to nat))) (d: nat) (t:
 285 T) on t: T \def (match t with [(TSort n) \Rightarrow (TSort n) | (TLRef i)
 286 \Rightarrow (TLRef (match (blt i d) with [true \Rightarrow i | false
 287 \Rightarrow (f i)])) | (THead k u t0) \Rightarrow (THead k (lref_map f d u)
 288 (lref_map f (s k d) t0))]) in lref_map) (\lambda (x: nat).(plus x h)) (r k0
 289 d) u0) | (CHead _ _ t) \Rightarrow t])) (CHead c0 k0 (lift h (r k0 d) u0))
 290 (CHead c k u) H7) in ((let H9 \def (f_equal C K (\lambda (e0: C).(match e0 in
 291 C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k _)
 292 \Rightarrow k])) (CHead c0 k0 (lift h (r k0 d) u0)) (CHead c k u) H7) in
 293 ((let H10 \def (f_equal C C (\lambda (e0: C).(match e0 in C return (\lambda
 294 (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c]))
 295 (CHead c0 k0 (lift h (r k0 d) u0)) (CHead c k u) H7) in (eq_ind C c (\lambda
 296 (c1: C).((eq K k0 k) \to ((eq T (lift h (r k0 d) u0) u) \to ((eq C (CHead e
 297 k0 u0) x) \to ((drop h (r k0 d) c1 e) \to (ex3_2 C T (\lambda (e0:
 298 C).(\lambda (v: T).(eq C x (CHead e0 k v)))) (\lambda (_: C).(\lambda (v:
 299 T).(eq T u (lift h (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r
 300 k d) c e0))))))))) (\lambda (H11: (eq K k0 k)).(eq_ind K k (\lambda (k1:
 301 K).((eq T (lift h (r k1 d) u0) u) \to ((eq C (CHead e k1 u0) x) \to ((drop h
 302 (r k1 d) c e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead
 303 e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k d) v))))
 304 (\lambda (e0: C).(\lambda (_: T).(drop h (r k d) c e0)))))))) (\lambda (H12:
 305 (eq T (lift h (r k d) u0) u)).(eq_ind T (lift h (r k d) u0) (\lambda (t:
 306 T).((eq C (CHead e k u0) x) \to ((drop h (r k d) c e) \to (ex3_2 C T (\lambda
 307 (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v)))) (\lambda (_: C).(\lambda
 308 (v: T).(eq T t (lift h (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h
 309 (r k d) c e0))))))) (\lambda (H13: (eq C (CHead e k u0) x)).(eq_ind C (CHead
 310 e k u0) (\lambda (c1: C).((drop h (r k d) c e) \to (ex3_2 C T (\lambda (e0:
 311 C).(\lambda (v: T).(eq C c1 (CHead e0 k v)))) (\lambda (_: C).(\lambda (v:
 312 T).(eq T (lift h (r k d) u0) (lift h (r k d) v)))) (\lambda (e0: C).(\lambda
 313 (_: T).(drop h (r k d) c e0)))))) (\lambda (H14: (drop h (r k d) c e)).(let
 314 H15 \def (eq_ind_r T u (\lambda (t: T).(drop h (S d) (CHead c k t) x)) H
 315 (lift h (r k d) u0) H12) in (let H16 \def (eq_ind_r C x (\lambda (c0:
 316 C).(drop h (S d) (CHead c k (lift h (r k d) u0)) c0)) H15 (CHead e k u0) H13)
 317 in (ex3_2_intro C T (\lambda (e0: C).(\lambda (v: T).(eq C (CHead e k u0)
 318 (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T (lift h (r k d) u0)
 319 (lift h (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r k d) c
 320 e0))) e u0 (refl_equal C (CHead e k u0)) (refl_equal T (lift h (r k d) u0))
 321 H14)))) x H13)) u H12)) k0 (sym_eq K k0 k H11))) c0 (sym_eq C c0 c H10)))
 322 H9)) H8))) d0 (sym_eq nat d0 d H6)))) h0 (sym_eq nat h0 h H1) H2 H3 H4
 323 H0)))))]) in (H0 (refl_equal nat h) (refl_equal nat (S d)) (refl_equal C
 324 (CHead c k u)) (refl_equal C x))))))))).
 325