helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/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/lift/fwd".
  18
  19 include "lift/defs.ma".
  20
  21 theorem lift_sort:
  22  \forall (n: nat).(\forall (h: nat).(\forall (d: nat).(eq T (lift h d (TSort
  23 n)) (TSort n))))
  24 \def
  25  \lambda (n: nat).(\lambda (_: nat).(\lambda (_: nat).(refl_equal T (TSort
  26 n)))).
  27
  28 theorem lift_lref_lt:
  29  \forall (n: nat).(\forall (h: nat).(\forall (d: nat).((lt n d) \to (eq T
  30 (lift h d (TLRef n)) (TLRef n)))))
  31 \def
  32  \lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (lt n
  33 d)).(eq_ind bool true (\lambda (b: bool).(eq T (TLRef (match b with [true
  34 \Rightarrow n | false \Rightarrow (plus n h)])) (TLRef n))) (refl_equal T
  35 (TLRef n)) (blt n d) (sym_equal bool (blt n d) true (lt_blt d n H)))))).
  36
  37 theorem lift_lref_ge:
  38  \forall (n: nat).(\forall (h: nat).(\forall (d: nat).((le d n) \to (eq T
  39 (lift h d (TLRef n)) (TLRef (plus n h))))))
  40 \def
  41  \lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (le d
  42 n)).(eq_ind bool false (\lambda (b: bool).(eq T (TLRef (match b with [true
  43 \Rightarrow n | false \Rightarrow (plus n h)])) (TLRef (plus n h))))
  44 (refl_equal T (TLRef (plus n h))) (blt n d) (sym_equal bool (blt n d) false
  45 (le_bge d n H)))))).
  46
  47 theorem lift_head:
  48  \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
  49 (d: nat).(eq T (lift h d (THead k u t)) (THead k (lift h d u) (lift h (s k d)
  50 t)))))))
  51 \def
  52  \lambda (k: K).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
  53 (d: nat).(refl_equal T (THead k (lift h d u) (lift h (s k d) t))))))).
  54
  55 theorem lift_bind:
  56  \forall (b: B).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
  57 (d: nat).(eq T (lift h d (THead (Bind b) u t)) (THead (Bind b) (lift h d u)
  58 (lift h (S d) t)))))))
  59 \def
  60  \lambda (b: B).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
  61 (d: nat).(refl_equal T (THead (Bind b) (lift h d u) (lift h (S d) t))))))).
  62
  63 theorem lift_flat:
  64  \forall (f: F).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
  65 (d: nat).(eq T (lift h d (THead (Flat f) u t)) (THead (Flat f) (lift h d u)
  66 (lift h d t)))))))
  67 \def
  68  \lambda (f: F).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
  69 (d: nat).(refl_equal T (THead (Flat f) (lift h d u) (lift h d t))))))).
  70
  71 theorem lift_gen_sort:
  72  \forall (h: nat).(\forall (d: nat).(\forall (n: nat).(\forall (t: T).((eq T
  73 (TSort n) (lift h d t)) \to (eq T t (TSort n))))))
  74 \def
  75  \lambda (h: nat).(\lambda (d: nat).(\lambda (n: nat).(\lambda (t: T).(T_ind
  76 (\lambda (t0: T).((eq T (TSort n) (lift h d t0)) \to (eq T t0 (TSort n))))
  77 (\lambda (n0: nat).(\lambda (H: (eq T (TSort n) (lift h d (TSort
  78 n0)))).(sym_eq T (TSort n) (TSort n0) H))) (\lambda (n0: nat).(\lambda (H:
  79 (eq T (TSort n) (lift h d (TLRef n0)))).(lt_le_e n0 d (eq T (TLRef n0) (TSort
  80 n)) (\lambda (H0: (lt n0 d)).(let H1 \def (eq_ind T (lift h d (TLRef n0))
  81 (\lambda (t: T).(eq T (TSort n) t)) H (TLRef n0) (lift_lref_lt n0 h d H0)) in
  82 (let H2 \def (match H1 in eq return (\lambda (t: T).(\lambda (_: (eq ? ?
  83 t)).((eq T t (TLRef n0)) \to (eq T (TLRef n0) (TSort n))))) with [refl_equal
  84 \Rightarrow (\lambda (H1: (eq T (TSort n) (TLRef n0))).(let H2 \def (eq_ind T
  85 (TSort n) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with
  86 [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _)
  87 \Rightarrow False])) I (TLRef n0) H1) in (False_ind (eq T (TLRef n0) (TSort
  88 n)) H2)))]) in (H2 (refl_equal T (TLRef n0)))))) (\lambda (H0: (le d
  89 n0)).(let H1 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T
  90 (TSort n) t)) H (TLRef (plus n0 h)) (lift_lref_ge n0 h d H0)) in (let H2 \def
  91 (match H1 in eq return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t
  92 (TLRef (plus n0 h))) \to (eq T (TLRef n0) (TSort n))))) with [refl_equal
  93 \Rightarrow (\lambda (H1: (eq T (TSort n) (TLRef (plus n0 h)))).(let H2 \def
  94 (eq_ind T (TSort n) (\lambda (e: T).(match e in T return (\lambda (_:
  95 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
  96 (THead _ _ _) \Rightarrow False])) I (TLRef (plus n0 h)) H1) in (False_ind
  97 (eq T (TLRef n0) (TSort n)) H2)))]) in (H2 (refl_equal T (TLRef (plus n0
  98 h)))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_: (((eq T (TSort n)
  99 (lift h d t0)) \to (eq T t0 (TSort n))))).(\lambda (t1: T).(\lambda (_: (((eq
 100 T (TSort n) (lift h d t1)) \to (eq T t1 (TSort n))))).(\lambda (H1: (eq T
 101 (TSort n) (lift h d (THead k t0 t1)))).(let H2 \def (eq_ind T (lift h d
 102 (THead k t0 t1)) (\lambda (t: T).(eq T (TSort n) t)) H1 (THead k (lift h d
 103 t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H3 \def (match H2
 104 in eq return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (THead k (lift
 105 h d t0) (lift h (s k d) t1))) \to (eq T (THead k t0 t1) (TSort n))))) with
 106 [refl_equal \Rightarrow (\lambda (H2: (eq T (TSort n) (THead k (lift h d t0)
 107 (lift h (s k d) t1)))).(let H3 \def (eq_ind T (TSort n) (\lambda (e:
 108 T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
 109 True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I
 110 (THead k (lift h d t0) (lift h (s k d) t1)) H2) in (False_ind (eq T (THead k
 111 t0 t1) (TSort n)) H3)))]) in (H3 (refl_equal T (THead k (lift h d t0) (lift h
 112 (s k d) t1)))))))))))) t)))).
 113
 114 theorem lift_gen_lref:
 115  \forall (t: T).(\forall (d: nat).(\forall (h: nat).(\forall (i: nat).((eq T
 116 (TLRef i) (lift h d t)) \to (or (land (lt i d) (eq T t (TLRef i))) (land (le
 117 (plus d h) i) (eq T t (TLRef (minus i h)))))))))
 118 \def
 119  \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (d: nat).(\forall (h:
 120 nat).(\forall (i: nat).((eq T (TLRef i) (lift h d t0)) \to (or (land (lt i d)
 121 (eq T t0 (TLRef i))) (land (le (plus d h) i) (eq T t0 (TLRef (minus i
 122 h)))))))))) (\lambda (n: nat).(\lambda (d: nat).(\lambda (h: nat).(\lambda
 123 (i: nat).(\lambda (H: (eq T (TLRef i) (lift h d (TSort n)))).(let H0 \def
 124 (eq_ind T (lift h d (TSort n)) (\lambda (t: T).(eq T (TLRef i) t)) H (TSort
 125 n) (lift_sort n h d)) in (let H1 \def (eq_ind T (TLRef i) (\lambda (ee:
 126 T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
 127 False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
 128 (TSort n) H0) in (False_ind (or (land (lt i d) (eq T (TSort n) (TLRef i)))
 129 (land (le (plus d h) i) (eq T (TSort n) (TLRef (minus i h))))) H1))))))))
 130 (\lambda (n: nat).(\lambda (d: nat).(\lambda (h: nat).(\lambda (i:
 131 nat).(\lambda (H: (eq T (TLRef i) (lift h d (TLRef n)))).(lt_le_e n d (or
 132 (land (lt i d) (eq T (TLRef n) (TLRef i))) (land (le (plus d h) i) (eq T
 133 (TLRef n) (TLRef (minus i h))))) (\lambda (H0: (lt n d)).(let H1 \def (eq_ind
 134 T (lift h d (TLRef n)) (\lambda (t: T).(eq T (TLRef i) t)) H (TLRef n)
 135 (lift_lref_lt n h d H0)) in (let H2 \def (f_equal T nat (\lambda (e:
 136 T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i |
 137 (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i])) (TLRef i) (TLRef n)
 138 H1) in (eq_ind_r nat n (\lambda (n0: nat).(or (land (lt n0 d) (eq T (TLRef n)
 139 (TLRef n0))) (land (le (plus d h) n0) (eq T (TLRef n) (TLRef (minus n0
 140 h)))))) (or_introl (land (lt n d) (eq T (TLRef n) (TLRef n))) (land (le (plus
 141 d h) n) (eq T (TLRef n) (TLRef (minus n h)))) (conj (lt n d) (eq T (TLRef n)
 142 (TLRef n)) H0 (refl_equal T (TLRef n)))) i H2)))) (\lambda (H0: (le d
 143 n)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t: T).(eq T (TLRef
 144 i) t)) H (TLRef (plus n h)) (lift_lref_ge n h d H0)) in (let H2 \def (f_equal
 145 T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort
 146 _) \Rightarrow i | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow i]))
 147 (TLRef i) (TLRef (plus n h)) H1) in (eq_ind_r nat (plus n h) (\lambda (n0:
 148 nat).(or (land (lt n0 d) (eq T (TLRef n) (TLRef n0))) (land (le (plus d h)
 149 n0) (eq T (TLRef n) (TLRef (minus n0 h)))))) (eq_ind_r nat n (\lambda (n0:
 150 nat).(or (land (lt (plus n h) d) (eq T (TLRef n) (TLRef (plus n h)))) (land
 151 (le (plus d h) (plus n h)) (eq T (TLRef n) (TLRef n0))))) (or_intror (land
 152 (lt (plus n h) d) (eq T (TLRef n) (TLRef (plus n h)))) (land (le (plus d h)
 153 (plus n h)) (eq T (TLRef n) (TLRef n))) (conj (le (plus d h) (plus n h)) (eq
 154 T (TLRef n) (TLRef n)) (plus_le_compat d n h h H0 (le_n h)) (refl_equal T
 155 (TLRef n)))) (minus (plus n h) h) (minus_plus_r n h)) i H2)))))))))) (\lambda
 156 (k: K).(\lambda (t0: T).(\lambda (_: ((\forall (d: nat).(\forall (h:
 157 nat).(\forall (i: nat).((eq T (TLRef i) (lift h d t0)) \to (or (land (lt i d)
 158 (eq T t0 (TLRef i))) (land (le (plus d h) i) (eq T t0 (TLRef (minus i
 159 h))))))))))).(\lambda (t1: T).(\lambda (_: ((\forall (d: nat).(\forall (h:
 160 nat).(\forall (i: nat).((eq T (TLRef i) (lift h d t1)) \to (or (land (lt i d)
 161 (eq T t1 (TLRef i))) (land (le (plus d h) i) (eq T t1 (TLRef (minus i
 162 h))))))))))).(\lambda (d: nat).(\lambda (h: nat).(\lambda (i: nat).(\lambda
 163 (H1: (eq T (TLRef i) (lift h d (THead k t0 t1)))).(let H2 \def (eq_ind T
 164 (lift h d (THead k t0 t1)) (\lambda (t: T).(eq T (TLRef i) t)) H1 (THead k
 165 (lift h d t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H3 \def
 166 (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_:
 167 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
 168 (THead _ _ _) \Rightarrow False])) I (THead k (lift h d t0) (lift h (s k d)
 169 t1)) H2) in (False_ind (or (land (lt i d) (eq T (THead k t0 t1) (TLRef i)))
 170 (land (le (plus d h) i) (eq T (THead k t0 t1) (TLRef (minus i h)))))
 171 H3)))))))))))) t).
 172
 173 theorem lift_gen_lref_lt:
 174  \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((lt n d) \to (\forall
 175 (t: T).((eq T (TLRef n) (lift h d t)) \to (eq T t (TLRef n)))))))
 176 \def
 177  \lambda (h: nat).(\lambda (d: nat).(\lambda (n: nat).(\lambda (H: (lt n
 178 d)).(\lambda (t: T).(T_ind (\lambda (t0: T).((eq T (TLRef n) (lift h d t0))
 179 \to (eq T t0 (TLRef n)))) (\lambda (n0: nat).(\lambda (H0: (eq T (TLRef n)
 180 (lift h d (TSort n0)))).(sym_eq T (TLRef n) (TSort n0) H0))) (\lambda (n0:
 181 nat).(\lambda (H0: (eq T (TLRef n) (lift h d (TLRef n0)))).(lt_le_e n0 d (eq
 182 T (TLRef n0) (TLRef n)) (\lambda (H1: (lt n0 d)).(let H2 \def (eq_ind T (lift
 183 h d (TLRef n0)) (\lambda (t: T).(eq T (TLRef n) t)) H0 (TLRef n0)
 184 (lift_lref_lt n0 h d H1)) in (sym_eq T (TLRef n) (TLRef n0) H2))) (\lambda
 185 (H1: (le d n0)).(let H2 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t:
 186 T).(eq T (TLRef n) t)) H0 (TLRef (plus n0 h)) (lift_lref_ge n0 h d H1)) in
 187 (let H3 \def (match H2 in eq return (\lambda (t: T).(\lambda (_: (eq ? ?
 188 t)).((eq T t (TLRef (plus n0 h))) \to (eq T (TLRef n0) (TLRef n))))) with
 189 [refl_equal \Rightarrow (\lambda (H2: (eq T (TLRef n) (TLRef (plus n0
 190 h)))).(let H3 \def (f_equal T nat (\lambda (e: T).(match e in T return
 191 (\lambda (_: T).nat) with [(TSort _) \Rightarrow n | (TLRef n) \Rightarrow n
 192 | (THead _ _ _) \Rightarrow n])) (TLRef n) (TLRef (plus n0 h)) H2) in (eq_ind
 193 nat (plus n0 h) (\lambda (n: nat).(eq T (TLRef n0) (TLRef n))) (let H0 \def
 194 (eq_ind nat n (\lambda (n: nat).(lt n d)) H (plus n0 h) H3) in (le_false d n0
 195 (eq T (TLRef n0) (TLRef (plus n0 h))) H1 (lt_le_S n0 d (le_lt_trans n0 (plus
 196 n0 h) d (le_plus_l n0 h) H0)))) n (sym_eq nat n (plus n0 h) H3))))]) in (H3
 197 (refl_equal T (TLRef (plus n0 h)))))))))) (\lambda (k: K).(\lambda (t0:
 198 T).(\lambda (_: (((eq T (TLRef n) (lift h d t0)) \to (eq T t0 (TLRef
 199 n))))).(\lambda (t1: T).(\lambda (_: (((eq T (TLRef n) (lift h d t1)) \to (eq
 200 T t1 (TLRef n))))).(\lambda (H2: (eq T (TLRef n) (lift h d (THead k t0
 201 t1)))).(let H3 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda (t: T).(eq
 202 T (TLRef n) t)) H2 (THead k (lift h d t0) (lift h (s k d) t1)) (lift_head k
 203 t0 t1 h d)) in (let H4 \def (match H3 in eq return (\lambda (t: T).(\lambda
 204 (_: (eq ? ? t)).((eq T t (THead k (lift h d t0) (lift h (s k d) t1))) \to (eq
 205 T (THead k t0 t1) (TLRef n))))) with [refl_equal \Rightarrow (\lambda (H3:
 206 (eq T (TLRef n) (THead k (lift h d t0) (lift h (s k d) t1)))).(let H4 \def
 207 (eq_ind T (TLRef n) (\lambda (e: T).(match e in T return (\lambda (_:
 208 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
 209 (THead _ _ _) \Rightarrow False])) I (THead k (lift h d t0) (lift h (s k d)
 210 t1)) H3) in (False_ind (eq T (THead k t0 t1) (TLRef n)) H4)))]) in (H4
 211 (refl_equal T (THead k (lift h d t0) (lift h (s k d) t1)))))))))))) t))))).
 212
 213 theorem lift_gen_lref_false:
 214  \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to ((lt n
 215 (plus d h)) \to (\forall (t: T).((eq T (TLRef n) (lift h d t)) \to (\forall
 216 (P: Prop).P)))))))
 217 \def
 218  \lambda (h: nat).(\lambda (d: nat).(\lambda (n: nat).(\lambda (H: (le d
 219 n)).(\lambda (H0: (lt n (plus d h))).(\lambda (t: T).(T_ind (\lambda (t0:
 220 T).((eq T (TLRef n) (lift h d t0)) \to (\forall (P: Prop).P))) (\lambda (n0:
 221 nat).(\lambda (H1: (eq T (TLRef n) (lift h d (TSort n0)))).(\lambda (P:
 222 Prop).(let H2 \def (match H1 in eq return (\lambda (t: T).(\lambda (_: (eq ?
 223 ? t)).((eq T t (lift h d (TSort n0))) \to P))) with [refl_equal \Rightarrow
 224 (\lambda (H2: (eq T (TLRef n) (lift h d (TSort n0)))).(let H3 \def (eq_ind T
 225 (TLRef n) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with
 226 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _)
 227 \Rightarrow False])) I (lift h d (TSort n0)) H2) in (False_ind P H3)))]) in
 228 (H2 (refl_equal T (lift h d (TSort n0)))))))) (\lambda (n0: nat).(\lambda
 229 (H1: (eq T (TLRef n) (lift h d (TLRef n0)))).(\lambda (P: Prop).(lt_le_e n0 d
 230 P (\lambda (H2: (lt n0 d)).(let H3 \def (eq_ind T (lift h d (TLRef n0))
 231 (\lambda (t: T).(eq T (TLRef n) t)) H1 (TLRef n0) (lift_lref_lt n0 h d H2))
 232 in (let H4 \def (match H3 in eq return (\lambda (t: T).(\lambda (_: (eq ? ?
 233 t)).((eq T t (TLRef n0)) \to P))) with [refl_equal \Rightarrow (\lambda (H3:
 234 (eq T (TLRef n) (TLRef n0))).(let H4 \def (f_equal T nat (\lambda (e:
 235 T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow n |
 236 (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow n])) (TLRef n) (TLRef n0)
 237 H3) in (eq_ind nat n0 (\lambda (_: nat).P) (let H1 \def (eq_ind_r nat n0
 238 (\lambda (n: nat).(lt n d)) H2 n H4) in (le_false d n P H H1)) n (sym_eq nat
 239 n n0 H4))))]) in (H4 (refl_equal T (TLRef n0)))))) (\lambda (H2: (le d
 240 n0)).(let H3 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T
 241 (TLRef n) t)) H1 (TLRef (plus n0 h)) (lift_lref_ge n0 h d H2)) in (let H4
 242 \def (match H3 in eq return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t
 243 (TLRef (plus n0 h))) \to P))) with [refl_equal \Rightarrow (\lambda (H3: (eq
 244 T (TLRef n) (TLRef (plus n0 h)))).(let H4 \def (f_equal T nat (\lambda (e:
 245 T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow n |
 246 (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow n])) (TLRef n) (TLRef
 247 (plus n0 h)) H3) in (eq_ind nat (plus n0 h) (\lambda (_: nat).P) (let H1 \def
 248 (eq_ind nat n (\lambda (n: nat).(lt n (plus d h))) H0 (plus n0 h) H4) in
 249 (le_false d n0 P H2 (lt_le_S n0 d (simpl_lt_plus_r h n0 d H1)))) n (sym_eq
 250 nat n (plus n0 h) H4))))]) in (H4 (refl_equal T (TLRef (plus n0 h)))))))))))
 251 (\lambda (k: K).(\lambda (t0: T).(\lambda (_: (((eq T (TLRef n) (lift h d
 252 t0)) \to (\forall (P: Prop).P)))).(\lambda (t1: T).(\lambda (_: (((eq T
 253 (TLRef n) (lift h d t1)) \to (\forall (P: Prop).P)))).(\lambda (H3: (eq T
 254 (TLRef n) (lift h d (THead k t0 t1)))).(\lambda (P: Prop).(let H4 \def
 255 (eq_ind T (lift h d (THead k t0 t1)) (\lambda (t: T).(eq T (TLRef n) t)) H3
 256 (THead k (lift h d t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in (let
 257 H5 \def (match H4 in eq return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq
 258 T t (THead k (lift h d t0) (lift h (s k d) t1))) \to P))) with [refl_equal
 259 \Rightarrow (\lambda (H4: (eq T (TLRef n) (THead k (lift h d t0) (lift h (s k
 260 d) t1)))).(let H5 \def (eq_ind T (TLRef n) (\lambda (e: T).(match e in T
 261 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
 262 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead k (lift h d
 263 t0) (lift h (s k d) t1)) H4) in (False_ind P H5)))]) in (H5 (refl_equal T
 264 (THead k (lift h d t0) (lift h (s k d) t1))))))))))))) t)))))).
 265
 266 theorem lift_gen_lref_ge:
 267  \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to (\forall
 268 (t: T).((eq T (TLRef (plus n h)) (lift h d t)) \to (eq T t (TLRef n)))))))
 269 \def
 270  \lambda (h: nat).(\lambda (d: nat).(\lambda (n: nat).(\lambda (H: (le d
 271 n)).(\lambda (t: T).(T_ind (\lambda (t0: T).((eq T (TLRef (plus n h)) (lift h
 272 d t0)) \to (eq T t0 (TLRef n)))) (\lambda (n0: nat).(\lambda (H0: (eq T
 273 (TLRef (plus n h)) (lift h d (TSort n0)))).(let H1 \def (match H0 in eq
 274 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (lift h d (TSort
 275 n0))) \to (eq T (TSort n0) (TLRef n))))) with [refl_equal \Rightarrow
 276 (\lambda (H1: (eq T (TLRef (plus n h)) (lift h d (TSort n0)))).(let H2 \def
 277 (eq_ind T (TLRef (plus n h)) (\lambda (e: T).(match e in T return (\lambda
 278 (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
 279 (THead _ _ _) \Rightarrow False])) I (lift h d (TSort n0)) H1) in (False_ind
 280 (eq T (TSort n0) (TLRef n)) H2)))]) in (H1 (refl_equal T (lift h d (TSort
 281 n0))))))) (\lambda (n0: nat).(\lambda (H0: (eq T (TLRef (plus n h)) (lift h d
 282 (TLRef n0)))).(lt_le_e n0 d (eq T (TLRef n0) (TLRef n)) (\lambda (H1: (lt n0
 283 d)).(let H2 \def (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T (TLRef
 284 (plus n h)) t)) H0 (TLRef n0) (lift_lref_lt n0 h d H1)) in (let H3 \def
 285 (match H2 in eq return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t
 286 (TLRef n0)) \to (eq T (TLRef n0) (TLRef n))))) with [refl_equal \Rightarrow
 287 (\lambda (H2: (eq T (TLRef (plus n h)) (TLRef n0))).(let H3 \def (f_equal T
 288 nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _)
 289 \Rightarrow ((let rec plus (n: nat) on n: (nat \to nat) \def (\lambda (m:
 290 nat).(match n with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in
 291 plus) n h) | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow ((let rec
 292 plus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n with [O
 293 \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in plus) n h)])) (TLRef
 294 (plus n h)) (TLRef n0) H2) in (eq_ind nat (plus n h) (\lambda (n0: nat).(eq T
 295 (TLRef n0) (TLRef n))) (let H0 \def (eq_ind_r nat n0 (\lambda (n: nat).(lt n
 296 d)) H1 (plus n h) H3) in (le_false d n (eq T (TLRef (plus n h)) (TLRef n)) H
 297 (lt_le_S n d (le_lt_trans n (plus n h) d (le_plus_l n h) H0)))) n0 H3)))]) in
 298 (H3 (refl_equal T (TLRef n0)))))) (\lambda (H1: (le d n0)).(let H2 \def
 299 (eq_ind T (lift h d (TLRef n0)) (\lambda (t: T).(eq T (TLRef (plus n h)) t))
 300 H0 (TLRef (plus n0 h)) (lift_lref_ge n0 h d H1)) in (let H3 \def (match H2 in
 301 eq return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (TLRef (plus n0
 302 h))) \to (eq T (TLRef n0) (TLRef n))))) with [refl_equal \Rightarrow (\lambda
 303 (H2: (eq T (TLRef (plus n h)) (TLRef (plus n0 h)))).(let H3 \def (f_equal T
 304 nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _)
 305 \Rightarrow ((let rec plus (n: nat) on n: (nat \to nat) \def (\lambda (m:
 306 nat).(match n with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in
 307 plus) n h) | (TLRef n) \Rightarrow n | (THead _ _ _) \Rightarrow ((let rec
 308 plus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n with [O
 309 \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in plus) n h)])) (TLRef
 310 (plus n h)) (TLRef (plus n0 h)) H2) in (eq_ind nat (plus n h) (\lambda (_:
 311 nat).(eq T (TLRef n0) (TLRef n))) (f_equal nat T TLRef n0 n (simpl_plus_r h
 312 n0 n (sym_eq nat (plus n h) (plus n0 h) H3))) (plus n0 h) H3)))]) in (H3
 313 (refl_equal T (TLRef (plus n0 h)))))))))) (\lambda (k: K).(\lambda (t0:
 314 T).(\lambda (_: (((eq T (TLRef (plus n h)) (lift h d t0)) \to (eq T t0 (TLRef
 315 n))))).(\lambda (t1: T).(\lambda (_: (((eq T (TLRef (plus n h)) (lift h d
 316 t1)) \to (eq T t1 (TLRef n))))).(\lambda (H2: (eq T (TLRef (plus n h)) (lift
 317 h d (THead k t0 t1)))).(let H3 \def (eq_ind T (lift h d (THead k t0 t1))
 318 (\lambda (t: T).(eq T (TLRef (plus n h)) t)) H2 (THead k (lift h d t0) (lift
 319 h (s k d) t1)) (lift_head k t0 t1 h d)) in (let H4 \def (match H3 in eq
 320 return (\lambda (t: T).(\lambda (_: (eq ? ? t)).((eq T t (THead k (lift h d
 321 t0) (lift h (s k d) t1))) \to (eq T (THead k t0 t1) (TLRef n))))) with
 322 [refl_equal \Rightarrow (\lambda (H3: (eq T (TLRef (plus n h)) (THead k (lift
 323 h d t0) (lift h (s k d) t1)))).(let H4 \def (eq_ind T (TLRef (plus n h))
 324 (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
 325 \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
 326 False])) I (THead k (lift h d t0) (lift h (s k d) t1)) H3) in (False_ind (eq
 327 T (THead k t0 t1) (TLRef n)) H4)))]) in (H4 (refl_equal T (THead k (lift h d
 328 t0) (lift h (s k d) t1)))))))))))) t))))).
 329
 330 theorem lift_gen_head:
 331  \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h:
 332 nat).(\forall (d: nat).((eq T (THead k u t) (lift h d x)) \to (ex3_2 T T
 333 (\lambda (y: T).(\lambda (z: T).(eq T x (THead k y z)))) (\lambda (y:
 334 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
 335 T).(eq T t (lift h (s k d) z)))))))))))
 336 \def
 337  \lambda (k: K).(\lambda (u: T).(\lambda (t: T).(\lambda (x: T).(T_ind
 338 (\lambda (t0: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead k u t)
 339 (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0 (THead
 340 k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda
 341 (_: T).(\lambda (z: T).(eq T t (lift h (s k d) z))))))))) (\lambda (n:
 342 nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead k u t)
 343 (lift h d (TSort n)))).(let H0 \def (match H in eq return (\lambda (t0:
 344 T).(\lambda (_: (eq ? ? t0)).((eq T t0 (lift h d (TSort n))) \to (ex3_2 T T
 345 (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead k y z)))) (\lambda (y:
 346 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
 347 T).(eq T t (lift h (s k d) z)))))))) with [refl_equal \Rightarrow (\lambda
 348 (H0: (eq T (THead k u t) (lift h d (TSort n)))).(let H1 \def (eq_ind T (THead
 349 k u t) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with
 350 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _)
 351 \Rightarrow True])) I (lift h d (TSort n)) H0) in (False_ind (ex3_2 T T
 352 (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead k y z)))) (\lambda (y:
 353 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
 354 T).(eq T t (lift h (s k d) z))))) H1)))]) in (H0 (refl_equal T (lift h d
 355 (TSort n))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d:
 356 nat).(\lambda (H: (eq T (THead k u t) (lift h d (TLRef n)))).(lt_le_e n d
 357 (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead k y z))))
 358 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
 359 T).(\lambda (z: T).(eq T t (lift h (s k d) z))))) (\lambda (H0: (lt n
 360 d)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t0: T).(eq T (THead
 361 k u t) t0)) H (TLRef n) (lift_lref_lt n h d H0)) in (let H2 \def (match H1 in
 362 eq return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef n)) \to
 363 (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead k y z))))
 364 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
 365 T).(\lambda (z: T).(eq T t (lift h (s k d) z)))))))) with [refl_equal
 366 \Rightarrow (\lambda (H1: (eq T (THead k u t) (TLRef n))).(let H2 \def
 367 (eq_ind T (THead k u t) (\lambda (e: T).(match e in T return (\lambda (_:
 368 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
 369 (THead _ _ _) \Rightarrow True])) I (TLRef n) H1) in (False_ind (ex3_2 T T
 370 (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead k y z)))) (\lambda (y:
 371 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
 372 T).(eq T t (lift h (s k d) z))))) H2)))]) in (H2 (refl_equal T (TLRef n))))))
 373 (\lambda (H0: (le d n)).(let H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda
 374 (t0: T).(eq T (THead k u t) t0)) H (TLRef (plus n h)) (lift_lref_ge n h d
 375 H0)) in (let H2 \def (match H1 in eq return (\lambda (t0: T).(\lambda (_: (eq
 376 ? ? t0)).((eq T t0 (TLRef (plus n h))) \to (ex3_2 T T (\lambda (y:
 377 T).(\lambda (z: T).(eq T (TLRef n) (THead k y z)))) (\lambda (y: T).(\lambda
 378 (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift
 379 h (s k d) z)))))))) with [refl_equal \Rightarrow (\lambda (H1: (eq T (THead k
 380 u t) (TLRef (plus n h)))).(let H2 \def (eq_ind T (THead k u t) (\lambda (e:
 381 T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
 382 False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I
 383 (TLRef (plus n h)) H1) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda (z:
 384 T).(eq T (TLRef n) (THead k y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u
 385 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k d)
 386 z))))) H2)))]) in (H2 (refl_equal T (TLRef (plus n h)))))))))))) (\lambda
 387 (k0: K).(\lambda (t0: T).(\lambda (_: ((\forall (h: nat).(\forall (d:
 388 nat).((eq T (THead k u t) (lift h d t0)) \to (ex3_2 T T (\lambda (y:
 389 T).(\lambda (z: T).(eq T t0 (THead k y z)))) (\lambda (y: T).(\lambda (_:
 390 T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s
 391 k d) z)))))))))).(\lambda (t1: T).(\lambda (_: ((\forall (h: nat).(\forall
 392 (d: nat).((eq T (THead k u t) (lift h d t1)) \to (ex3_2 T T (\lambda (y:
 393 T).(\lambda (z: T).(eq T t1 (THead k y z)))) (\lambda (y: T).(\lambda (_:
 394 T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s
 395 k d) z)))))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (eq T
 396 (THead k u t) (lift h d (THead k0 t0 t1)))).(let H2 \def (eq_ind T (lift h d
 397 (THead k0 t0 t1)) (\lambda (t0: T).(eq T (THead k u t) t0)) H1 (THead k0
 398 (lift h d t0) (lift h (s k0 d) t1)) (lift_head k0 t0 t1 h d)) in (let H3 \def
 399 (match H2 in eq return (\lambda (t2: T).(\lambda (_: (eq ? ? t2)).((eq T t2
 400 (THead k0 (lift h d t0) (lift h (s k0 d) t1))) \to (ex3_2 T T (\lambda (y:
 401 T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead k y z)))) (\lambda (y:
 402 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
 403 T).(eq T t (lift h (s k d) z)))))))) with [refl_equal \Rightarrow (\lambda
 404 (H2: (eq T (THead k u t) (THead k0 (lift h d t0) (lift h (s k0 d) t1)))).(let
 405 H3 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
 406 with [(TSort _) \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ _ t)
 407 \Rightarrow t])) (THead k u t) (THead k0 (lift h d t0) (lift h (s k0 d) t1))
 408 H2) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e in T return
 409 (\lambda (_: T).T) with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u |
 410 (THead _ t _) \Rightarrow t])) (THead k u t) (THead k0 (lift h d t0) (lift h
 411 (s k0 d) t1)) H2) in ((let H5 \def (f_equal T K (\lambda (e: T).(match e in T
 412 return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _)
 413 \Rightarrow k | (THead k _ _) \Rightarrow k])) (THead k u t) (THead k0 (lift
 414 h d t0) (lift h (s k0 d) t1)) H2) in (eq_ind K k0 (\lambda (k: K).((eq T u
 415 (lift h d t0)) \to ((eq T t (lift h (s k0 d) t1)) \to (ex3_2 T T (\lambda (y:
 416 T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead k y z)))) (\lambda (y:
 417 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
 418 T).(eq T t (lift h (s k d) z)))))))) (\lambda (H6: (eq T u (lift h d
 419 t0))).(eq_ind T (lift h d t0) (\lambda (t2: T).((eq T t (lift h (s k0 d) t1))
 420 \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead
 421 k0 y z)))) (\lambda (y: T).(\lambda (_: T).(eq T t2 (lift h d y)))) (\lambda
 422 (_: T).(\lambda (z: T).(eq T t (lift h (s k0 d) z))))))) (\lambda (H7: (eq T
 423 t (lift h (s k0 d) t1))).(eq_ind T (lift h (s k0 d) t1) (\lambda (t:
 424 T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead
 425 k0 y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0) (lift h d
 426 y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (s k0 d) z))))))
 427 (ex3_2_intro T T (\lambda (y: T).(\lambda (z: T).(eq T (THead k0 t0 t1)
 428 (THead k0 y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0) (lift h
 429 d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (s k0 d) t1) (lift h (s
 430 k0 d) z)))) t0 t1 (refl_equal T (THead k0 t0 t1)) (refl_equal T (lift h d
 431 t0)) (refl_equal T (lift h (s k0 d) t1))) t (sym_eq T t (lift h (s k0 d) t1)
 432 H7))) u (sym_eq T u (lift h d t0) H6))) k (sym_eq K k k0 H5))) H4)) H3)))])
 433 in (H3 (refl_equal T (THead k0 (lift h d t0) (lift h (s k0 d)
 434 t1)))))))))))))) x)))).
 435
 436 theorem lift_gen_bind:
 437  \forall (b: B).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h:
 438 nat).(\forall (d: nat).((eq T (THead (Bind b) u t) (lift h d x)) \to (ex3_2 T
 439 T (\lambda (y: T).(\lambda (z: T).(eq T x (THead (Bind b) y z)))) (\lambda
 440 (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
 441 T).(eq T t (lift h (S d) z)))))))))))
 442 \def
 443  \lambda (b: B).(\lambda (u: T).(\lambda (t: T).(\lambda (x: T).(T_ind
 444 (\lambda (t0: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead (Bind b) u
 445 t) (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0
 446 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d
 447 y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))))
 448 (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T
 449 (THead (Bind b) u t) (lift h d (TSort n)))).(let H0 \def (match H in eq
 450 return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (lift h d (TSort
 451 n))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead
 452 (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y))))
 453 (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))) with
 454 [refl_equal \Rightarrow (\lambda (H0: (eq T (THead (Bind b) u t) (lift h d
 455 (TSort n)))).(let H1 \def (eq_ind T (THead (Bind b) u t) (\lambda (e:
 456 T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
 457 False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I
 458 (lift h d (TSort n)) H0) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda
 459 (z: T).(eq T (TSort n) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_:
 460 T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S
 461 d) z))))) H1)))]) in (H0 (refl_equal T (lift h d (TSort n))))))))) (\lambda
 462 (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead (Bind
 463 b) u t) (lift h d (TLRef n)))).(lt_le_e n d (ex3_2 T T (\lambda (y:
 464 T).(\lambda (z: T).(eq T (TLRef n) (THead (Bind b) y z)))) (\lambda (y:
 465 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
 466 T).(eq T t (lift h (S d) z))))) (\lambda (H0: (lt n d)).(let H1 \def (eq_ind
 467 T (lift h d (TLRef n)) (\lambda (t0: T).(eq T (THead (Bind b) u t) t0)) H
 468 (TLRef n) (lift_lref_lt n h d H0)) in (let H2 \def (match H1 in eq return
 469 (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef n)) \to (ex3_2 T
 470 T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Bind b) y z))))
 471 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
 472 T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))) with [refl_equal
 473 \Rightarrow (\lambda (H1: (eq T (THead (Bind b) u t) (TLRef n))).(let H2 \def
 474 (eq_ind T (THead (Bind b) u t) (\lambda (e: T).(match e in T return (\lambda
 475 (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
 476 | (THead _ _ _) \Rightarrow True])) I (TLRef n) H1) in (False_ind (ex3_2 T T
 477 (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Bind b) y z))))
 478 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
 479 T).(\lambda (z: T).(eq T t (lift h (S d) z))))) H2)))]) in (H2 (refl_equal T
 480 (TLRef n)))))) (\lambda (H0: (le d n)).(let H1 \def (eq_ind T (lift h d
 481 (TLRef n)) (\lambda (t0: T).(eq T (THead (Bind b) u t) t0)) H (TLRef (plus n
 482 h)) (lift_lref_ge n h d H0)) in (let H2 \def (match H1 in eq return (\lambda
 483 (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef (plus n h))) \to (ex3_2 T
 484 T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Bind b) y z))))
 485 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
 486 T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))) with [refl_equal
 487 \Rightarrow (\lambda (H1: (eq T (THead (Bind b) u t) (TLRef (plus n
 488 h)))).(let H2 \def (eq_ind T (THead (Bind b) u t) (\lambda (e: T).(match e in
 489 T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
 490 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef (plus n h))
 491 H1) in (False_ind (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n)
 492 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d
 493 y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z))))) H2)))]) in
 494 (H2 (refl_equal T (TLRef (plus n h)))))))))))) (\lambda (k: K).(\lambda (t0:
 495 T).(\lambda (_: ((\forall (h: nat).(\forall (d: nat).((eq T (THead (Bind b) u
 496 t) (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0
 497 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d
 498 y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d)
 499 z)))))))))).(\lambda (t1: T).(\lambda (_: ((\forall (h: nat).(\forall (d:
 500 nat).((eq T (THead (Bind b) u t) (lift h d t1)) \to (ex3_2 T T (\lambda (y:
 501 T).(\lambda (z: T).(eq T t1 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda
 502 (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift
 503 h (S d) z)))))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (eq T
 504 (THead (Bind b) u t) (lift h d (THead k t0 t1)))).(let H2 \def (eq_ind T
 505 (lift h d (THead k t0 t1)) (\lambda (t0: T).(eq T (THead (Bind b) u t) t0))
 506 H1 (THead k (lift h d t0) (lift h (s k d) t1)) (lift_head k t0 t1 h d)) in
 507 (let H3 \def (match H2 in eq return (\lambda (t2: T).(\lambda (_: (eq ? ?
 508 t2)).((eq T t2 (THead k (lift h d t0) (lift h (s k d) t1))) \to (ex3_2 T T
 509 (\lambda (y: T).(\lambda (z: T).(eq T (THead k t0 t1) (THead (Bind b) y z))))
 510 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
 511 T).(\lambda (z: T).(eq T t (lift h (S d) z)))))))) with [refl_equal
 512 \Rightarrow (\lambda (H2: (eq T (THead (Bind b) u t) (THead k (lift h d t0)
 513 (lift h (s k d) t1)))).(let H3 \def (f_equal T T (\lambda (e: T).(match e in
 514 T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _)
 515 \Rightarrow t | (THead _ _ t) \Rightarrow t])) (THead (Bind b) u t) (THead k
 516 (lift h d t0) (lift h (s k d) t1)) H2) in ((let H4 \def (f_equal T T (\lambda
 517 (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u
 518 | (TLRef _) \Rightarrow u | (THead _ t _) \Rightarrow t])) (THead (Bind b) u
 519 t) (THead k (lift h d t0) (lift h (s k d) t1)) H2) in ((let H5 \def (f_equal
 520 T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _)
 521 \Rightarrow (Bind b) | (TLRef _) \Rightarrow (Bind b) | (THead k _ _)
 522 \Rightarrow k])) (THead (Bind b) u t) (THead k (lift h d t0) (lift h (s k d)
 523 t1)) H2) in (eq_ind K (Bind b) (\lambda (k: K).((eq T u (lift h d t0)) \to
 524 ((eq T t (lift h (s k d) t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z:
 525 T).(eq T (THead k t0 t1) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_:
 526 T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S
 527 d) z)))))))) (\lambda (H6: (eq T u (lift h d t0))).(eq_ind T (lift h d t0)
 528 (\lambda (t2: T).((eq T t (lift h (s (Bind b) d) t1)) \to (ex3_2 T T (\lambda
 529 (y: T).(\lambda (z: T).(eq T (THead (Bind b) t0 t1) (THead (Bind b) y z))))
 530 (\lambda (y: T).(\lambda (_: T).(eq T t2 (lift h d y)))) (\lambda (_:
 531 T).(\lambda (z: T).(eq T t (lift h (S d) z))))))) (\lambda (H7: (eq T t (lift
 532 h (s (Bind b) d) t1))).(eq_ind T (lift h (s (Bind b) d) t1) (\lambda (t:
 533 T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Bind b) t0 t1)
 534 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0)
 535 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z))))))
 536 (ex3_2_intro T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Bind b) t0 t1)
 537 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d t0)
 538 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (s (Bind b) d)
 539 t1) (lift h (S d) z)))) t0 t1 (refl_equal T (THead (Bind b) t0 t1))
 540 (refl_equal T (lift h d t0)) (refl_equal T (lift h (S d) t1))) t (sym_eq T t
 541 (lift h (s (Bind b) d) t1) H7))) u (sym_eq T u (lift h d t0) H6))) k H5))
 542 H4)) H3)))]) in (H3 (refl_equal T (THead k (lift h d t0) (lift h (s k d)
 543 t1)))))))))))))) x)))).
 544
 545 theorem lift_gen_flat:
 546  \forall (f: F).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h:
 547 nat).(\forall (d: nat).((eq T (THead (Flat f) u t) (lift h d x)) \to (ex3_2 T
 548 T (\lambda (y: T).(\lambda (z: T).(eq T x (THead (Flat f) y z)))) (\lambda
 549 (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
 550 T).(eq T t (lift h d z)))))))))))
 551 \def
 552  \lambda (f: F).(\lambda (u: T).(\lambda (t: T).(\lambda (x: T).(T_ind
 553 (\lambda (t0: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead (Flat f) u
 554 t) (lift h d t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0
 555 (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d
 556 y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z))))))))) (\lambda
 557 (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (eq T (THead (Flat
 558 f) u t) (lift h d (TSort n)))).(let H0 \def (match H in eq return (\lambda
 559 (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (lift h d (TSort n))) \to (ex3_2
 560 T T (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead (Flat f) y z))))
 561 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
 562 T).(\lambda (z: T).(eq T t (lift h d z)))))))) with [refl_equal \Rightarrow
 563 (\lambda (H0: (eq T (THead (Flat f) u t) (lift h d (TSort n)))).(let H1 \def
 564 (eq_ind T (THead (Flat f) u t) (\lambda (e: T).(match e in T return (\lambda
 565 (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
 566 | (THead _ _ _) \Rightarrow True])) I (lift h d (TSort n)) H0) in (False_ind
 567 (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TSort n) (THead (Flat f) y
 568 z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
 569 T).(\lambda (z: T).(eq T t (lift h d z))))) H1)))]) in (H0 (refl_equal T
 570 (lift h d (TSort n))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d:
 571 nat).(\lambda (H: (eq T (THead (Flat f) u t) (lift h d (TLRef n)))).(lt_le_e
 572 n d (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat
 573 f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda
 574 (_: T).(\lambda (z: T).(eq T t (lift h d z))))) (\lambda (H0: (lt n d)).(let
 575 H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t0: T).(eq T (THead (Flat f)
 576 u t) t0)) H (TLRef n) (lift_lref_lt n h d H0)) in (let H2 \def (match H1 in
 577 eq return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef n)) \to
 578 (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y
 579 z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
 580 T).(\lambda (z: T).(eq T t (lift h d z)))))))) with [refl_equal \Rightarrow
 581 (\lambda (H1: (eq T (THead (Flat f) u t) (TLRef n))).(let H2 \def (eq_ind T
 582 (THead (Flat f) u t) (\lambda (e: T).(match e in T return (\lambda (_:
 583 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
 584 (THead _ _ _) \Rightarrow True])) I (TLRef n) H1) in (False_ind (ex3_2 T T
 585 (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y z))))
 586 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
 587 T).(\lambda (z: T).(eq T t (lift h d z))))) H2)))]) in (H2 (refl_equal T
 588 (TLRef n)))))) (\lambda (H0: (le d n)).(let H1 \def (eq_ind T (lift h d
 589 (TLRef n)) (\lambda (t0: T).(eq T (THead (Flat f) u t) t0)) H (TLRef (plus n
 590 h)) (lift_lref_ge n h d H0)) in (let H2 \def (match H1 in eq return (\lambda
 591 (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef (plus n h))) \to (ex3_2 T
 592 T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y z))))
 593 (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
 594 T).(\lambda (z: T).(eq T t (lift h d z)))))))) with [refl_equal \Rightarrow
 595 (\lambda (H1: (eq T (THead (Flat f) u t) (TLRef (plus n h)))).(let H2 \def
 596 (eq_ind T (THead (Flat f) u t) (\lambda (e: T).(match e in T return (\lambda
 597 (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
 598 | (THead _ _ _) \Rightarrow True])) I (TLRef (plus n h)) H1) in (False_ind
 599 (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y
 600 z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
 601 T).(\lambda (z: T).(eq T t (lift h d z))))) H2)))]) in (H2 (refl_equal T
 602 (TLRef (plus n h)))))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_:
 603 ((\forall (h: nat).(\forall (d: nat).((eq T (THead (Flat f) u t) (lift h d
 604 t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0 (THead (Flat f)
 605 y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
 606 T).(\lambda (z: T).(eq T t (lift h d z)))))))))).(\lambda (t1: T).(\lambda
 607 (_: ((\forall (h: nat).(\forall (d: nat).((eq T (THead (Flat f) u t) (lift h
 608 d t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t1 (THead (Flat
 609 f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda
 610 (_: T).(\lambda (z: T).(eq T t (lift h d z)))))))))).(\lambda (h:
 611 nat).(\lambda (d: nat).(\lambda (H1: (eq T (THead (Flat f) u t) (lift h d
 612 (THead k t0 t1)))).(let H2 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda
 613 (t0: T).(eq T (THead (Flat f) u t) t0)) H1 (THead k (lift h d t0) (lift h (s
 614 k d) t1)) (lift_head k t0 t1 h d)) in (let H3 \def (match H2 in eq return
 615 (\lambda (t2: T).(\lambda (_: (eq ? ? t2)).((eq T t2 (THead k (lift h d t0)
 616 (lift h (s k d) t1))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T
 617 (THead k t0 t1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T
 618 u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z))))))))
 619 with [refl_equal \Rightarrow (\lambda (H2: (eq T (THead (Flat f) u t) (THead
 620 k (lift h d t0) (lift h (s k d) t1)))).(let H3 \def (f_equal T T (\lambda (e:
 621 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t |
 622 (TLRef _) \Rightarrow t | (THead _ _ t) \Rightarrow t])) (THead (Flat f) u t)
 623 (THead k (lift h d t0) (lift h (s k d) t1)) H2) in ((let H4 \def (f_equal T T
 624 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
 625 \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t _) \Rightarrow t]))
 626 (THead (Flat f) u t) (THead k (lift h d t0) (lift h (s k d) t1)) H2) in ((let
 627 H5 \def (f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K)
 628 with [(TSort _) \Rightarrow (Flat f) | (TLRef _) \Rightarrow (Flat f) |
 629 (THead k _ _) \Rightarrow k])) (THead (Flat f) u t) (THead k (lift h d t0)
 630 (lift h (s k d) t1)) H2) in (eq_ind K (Flat f) (\lambda (k: K).((eq T u (lift
 631 h d t0)) \to ((eq T t (lift h (s k d) t1)) \to (ex3_2 T T (\lambda (y:
 632 T).(\lambda (z: T).(eq T (THead k t0 t1) (THead (Flat f) y z)))) (\lambda (y:
 633 T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z:
 634 T).(eq T t (lift h d z)))))))) (\lambda (H6: (eq T u (lift h d t0))).(eq_ind
 635 T (lift h d t0) (\lambda (t2: T).((eq T t (lift h (s (Flat f) d) t1)) \to
 636 (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Flat f) t0 t1)
 637 (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T t2 (lift h d
 638 y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z))))))) (\lambda
 639 (H7: (eq T t (lift h (s (Flat f) d) t1))).(eq_ind T (lift h (s (Flat f) d)
 640 t1) (\lambda (t: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead
 641 (Flat f) t0 t1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T
 642 (lift h d t0) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h
 643 d z)))))) (ex3_2_intro T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Flat
 644 f) t0 t1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift
 645 h d t0) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (s
 646 (Flat f) d) t1) (lift h d z)))) t0 t1 (refl_equal T (THead (Flat f) t0 t1))
 647 (refl_equal T (lift h d t0)) (refl_equal T (lift h d t1))) t (sym_eq T t
 648 (lift h (s (Flat f) d) t1) H7))) u (sym_eq T u (lift h d t0) H6))) k H5))
 649 H4)) H3)))]) in (H3 (refl_equal T (THead k (lift h d t0) (lift h (s k d)
 650 t1)))))))))))))) x)))).
 651