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