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

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "basic_1A/lift/defs.ma".
  18
  19 include "basic_1A/s/props.ma".
  20
  21 include "basic_1A/T/fwd.ma".
  22
  23 lemma lift_sort:
  24  \forall (n: nat).(\forall (h: nat).(\forall (d: nat).(eq T (lift h d (TSort
  25 n)) (TSort n))))
  26 \def
  27  \lambda (n: nat).(\lambda (_: nat).(\lambda (_: nat).(refl_equal T (TSort
  28 n)))).
  29
  30 lemma lift_lref_lt:
  31  \forall (n: nat).(\forall (h: nat).(\forall (d: nat).((lt n d) \to (eq T
  32 (lift h d (TLRef n)) (TLRef n)))))
  33 \def
  34  \lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (lt n
  35 d)).(eq_ind bool true (\lambda (b: bool).(eq T (TLRef (match b with [true
  36 \Rightarrow n | false \Rightarrow (plus n h)])) (TLRef n))) (refl_equal T
  37 (TLRef n)) (blt n d) (sym_eq bool (blt n d) true (lt_blt d n H)))))).
  38
  39 lemma lift_lref_ge:
  40  \forall (n: nat).(\forall (h: nat).(\forall (d: nat).((le d n) \to (eq T
  41 (lift h d (TLRef n)) (TLRef (plus n h))))))
  42 \def
  43  \lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (le d
  44 n)).(eq_ind bool false (\lambda (b: bool).(eq T (TLRef (match b with [true
  45 \Rightarrow n | false \Rightarrow (plus n h)])) (TLRef (plus n h))))
  46 (refl_equal T (TLRef (plus n h))) (blt n d) (sym_eq bool (blt n d) false
  47 (le_bge d n H)))))).
  48
  49 lemma lift_head:
  50  \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
  51 (d: nat).(eq T (lift h d (THead k u t)) (THead k (lift h d u) (lift h (s k d)
  52 t)))))))
  53 \def
  54  \lambda (k: K).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
  55 (d: nat).(refl_equal T (THead k (lift h d u) (lift h (s k d) t))))))).
  56
  57 lemma lift_bind:
  58  \forall (b: B).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
  59 (d: nat).(eq T (lift h d (THead (Bind b) u t)) (THead (Bind b) (lift h d u)
  60 (lift h (S d) t)))))))
  61 \def
  62  \lambda (b: B).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
  63 (d: nat).(refl_equal T (THead (Bind b) (lift h d u) (lift h (S d) t))))))).
  64
  65 lemma lift_flat:
  66  \forall (f: F).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
  67 (d: nat).(eq T (lift h d (THead (Flat f) u t)) (THead (Flat f) (lift h d u)
  68 (lift h d t)))))))
  69 \def
  70  \lambda (f: F).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
  71 (d: nat).(refl_equal T (THead (Flat f) (lift h d u) (lift h d t))))))).
  72
  73 lemma thead_x_lift_y_y:
  74  \forall (k: K).(\forall (t: T).(\forall (v: T).(\forall (h: nat).(\forall
  75 (d: nat).((eq T (THead k v (lift h d t)) t) \to (\forall (P: Prop).P))))))
  76 \def
  77  \lambda (k: K).(\lambda (t: T).(T_ind (\lambda (t0: T).(\forall (v:
  78 T).(\forall (h: nat).(\forall (d: nat).((eq T (THead k v (lift h d t0)) t0)
  79 \to (\forall (P: Prop).P)))))) (\lambda (n: nat).(\lambda (v: T).(\lambda (h:
  80 nat).(\lambda (d: nat).(\lambda (H: (eq T (THead k v (lift h d (TSort n)))
  81 (TSort n))).(\lambda (P: Prop).(let H0 \def (eq_ind T (THead k v (lift h d
  82 (TSort n))) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
  83 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n)
  84 H) in (False_ind P H0)))))))) (\lambda (n: nat).(\lambda (v: T).(\lambda (h:
  85 nat).(\lambda (d: nat).(\lambda (H: (eq T (THead k v (lift h d (TLRef n)))
  86 (TLRef n))).(\lambda (P: Prop).(let H0 \def (eq_ind T (THead k v (lift h d
  87 (TLRef n))) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
  88 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n)
  89 H) in (False_ind P H0)))))))) (\lambda (k0: K).(\lambda (t0: T).(\lambda (_:
  90 ((\forall (v: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead k v (lift
  91 h d t0)) t0) \to (\forall (P: Prop).P))))))).(\lambda (t1: T).(\lambda (H0:
  92 ((\forall (v: T).(\forall (h: nat).(\forall (d: nat).((eq T (THead k v (lift
  93 h d t1)) t1) \to (\forall (P: Prop).P))))))).(\lambda (v: T).(\lambda (h:
  94 nat).(\lambda (d: nat).(\lambda (H1: (eq T (THead k v (lift h d (THead k0 t0
  95 t1))) (THead k0 t0 t1))).(\lambda (P: Prop).(let H2 \def (f_equal T K
  96 (\lambda (e: T).(match e with [(TSort _) \Rightarrow k | (TLRef _)
  97 \Rightarrow k | (THead k1 _ _) \Rightarrow k1])) (THead k v (lift h d (THead
  98 k0 t0 t1))) (THead k0 t0 t1) H1) in ((let H3 \def (f_equal T T (\lambda (e:
  99 T).(match e with [(TSort _) \Rightarrow v | (TLRef _) \Rightarrow v | (THead
 100 _ t2 _) \Rightarrow t2])) (THead k v (lift h d (THead k0 t0 t1))) (THead k0
 101 t0 t1) H1) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e with
 102 [(TSort _) \Rightarrow (THead k0 (lref_map (\lambda (x: nat).(plus x h)) d
 103 t0) (lref_map (\lambda (x: nat).(plus x h)) (s k0 d) t1)) | (TLRef _)
 104 \Rightarrow (THead k0 (lref_map (\lambda (x: nat).(plus x h)) d t0) (lref_map
 105 (\lambda (x: nat).(plus x h)) (s k0 d) t1)) | (THead _ _ t2) \Rightarrow
 106 t2])) (THead k v (lift h d (THead k0 t0 t1))) (THead k0 t0 t1) H1) in
 107 (\lambda (_: (eq T v t0)).(\lambda (H6: (eq K k k0)).(let H7 \def (eq_ind K k
 108 (\lambda (k1: K).(\forall (v0: T).(\forall (h0: nat).(\forall (d0: nat).((eq
 109 T (THead k1 v0 (lift h0 d0 t1)) t1) \to (\forall (P0: Prop).P0)))))) H0 k0
 110 H6) in (let H8 \def (eq_ind T (lift h d (THead k0 t0 t1)) (\lambda (t2:
 111 T).(eq T t2 t1)) H4 (THead k0 (lift h d t0) (lift h (s k0 d) t1)) (lift_head
 112 k0 t0 t1 h d)) in (H7 (lift h d t0) h (s k0 d) H8 P)))))) H3)) H2))))))))))))
 113 t)).
 114
 115 lemma lift_r:
 116  \forall (t: T).(\forall (d: nat).(eq T (lift O d t) t))
 117 \def
 118  \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (d: nat).(eq T (lift O d t0)
 119 t0))) (\lambda (n: nat).(\lambda (_: nat).(refl_equal T (TSort n)))) (\lambda
 120 (n: nat).(\lambda (d: nat).(lt_le_e n d (eq T (lift O d (TLRef n)) (TLRef n))
 121 (\lambda (H: (lt n d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0 (TLRef
 122 n))) (refl_equal T (TLRef n)) (lift O d (TLRef n)) (lift_lref_lt n O d H)))
 123 (\lambda (H: (le d n)).(eq_ind_r T (TLRef (plus n O)) (\lambda (t0: T).(eq T
 124 t0 (TLRef n))) (f_equal nat T TLRef (plus n O) n (sym_eq nat n (plus n O)
 125 (plus_n_O n))) (lift O d (TLRef n)) (lift_lref_ge n O d H)))))) (\lambda (k:
 126 K).(\lambda (t0: T).(\lambda (H: ((\forall (d: nat).(eq T (lift O d t0)
 127 t0)))).(\lambda (t1: T).(\lambda (H0: ((\forall (d: nat).(eq T (lift O d t1)
 128 t1)))).(\lambda (d: nat).(eq_ind_r T (THead k (lift O d t0) (lift O (s k d)
 129 t1)) (\lambda (t2: T).(eq T t2 (THead k t0 t1))) (sym_eq T (THead k t0 t1)
 130 (THead k (lift O d t0) (lift O (s k d) t1)) (sym_eq T (THead k (lift O d t0)
 131 (lift O (s k d) t1)) (THead k t0 t1) (f_equal3 K T T T THead k k (lift O d
 132 t0) t0 (lift O (s k d) t1) t1 (refl_equal K k) (H d) (H0 (s k d))))) (lift O
 133 d (THead k t0 t1)) (lift_head k t0 t1 O d)))))))) t).
 134
 135 lemma lift_lref_gt:
 136  \forall (d: nat).(\forall (n: nat).((lt d n) \to (eq T (lift (S O) d (TLRef
 137 (pred n))) (TLRef n))))
 138 \def
 139  \lambda (d: nat).(\lambda (n: nat).(\lambda (H: (lt d n)).(eq_ind_r T (TLRef
 140 (plus (pred n) (S O))) (\lambda (t: T).(eq T t (TLRef n))) (eq_ind nat (plus
 141 (S O) (pred n)) (\lambda (n0: nat).(eq T (TLRef n0) (TLRef n))) (eq_ind nat n
 142 (\lambda (n0: nat).(eq T (TLRef n0) (TLRef n))) (refl_equal T (TLRef n)) (S
 143 (pred n)) (S_pred n d H)) (plus (pred n) (S O)) (plus_sym (S O) (pred n)))
 144 (lift (S O) d (TLRef (pred n))) (lift_lref_ge (pred n) (S O) d (le_S_n d
 145 (pred n) (eq_ind nat n (\lambda (n0: nat).(le (S d) n0)) H (S (pred n))
 146 (S_pred n d H))))))).
 147
 148 lemma lift_tle:
 149  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(tle t (lift h d t))))
 150 \def
 151  \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (h: nat).(\forall (d:
 152 nat).(le (tweight t0) (tweight (lift h d t0)))))) (\lambda (_: nat).(\lambda
 153 (_: nat).(\lambda (_: nat).(le_n (S O))))) (\lambda (_: nat).(\lambda (_:
 154 nat).(\lambda (_: nat).(le_n (S O))))) (\lambda (k: K).(\lambda (t0:
 155 T).(\lambda (H: ((\forall (h: nat).(\forall (d: nat).(le (tweight t0)
 156 (tweight (lift h d t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (h:
 157 nat).(\forall (d: nat).(le (tweight t1) (tweight (lift h d t1))))))).(\lambda
 158 (h: nat).(\lambda (d: nat).(let H_y \def (H h d) in (let H_y0 \def (H0 h (s k
 159 d)) in (le_n_S (plus (tweight t0) (tweight t1)) (plus (tweight (lref_map
 160 (\lambda (x: nat).(plus x h)) d t0)) (tweight (lref_map (\lambda (x:
 161 nat).(plus x h)) (s k d) t1))) (le_plus_plus (tweight t0) (tweight (lref_map
 162 (\lambda (x: nat).(plus x h)) d t0)) (tweight t1) (tweight (lref_map (\lambda
 163 (x: nat).(plus x h)) (s k d) t1)) H_y H_y0))))))))))) t).
 164
 165 lemma lifts_tapp:
 166  \forall (h: nat).(\forall (d: nat).(\forall (v: T).(\forall (vs: TList).(eq
 167 TList (lifts h d (TApp vs v)) (TApp (lifts h d vs) (lift h d v))))))
 168 \def
 169  \lambda (h: nat).(\lambda (d: nat).(\lambda (v: T).(\lambda (vs:
 170 TList).(TList_ind (\lambda (t: TList).(eq TList (lifts h d (TApp t v)) (TApp
 171 (lifts h d t) (lift h d v)))) (refl_equal TList (TCons (lift h d v) TNil))
 172 (\lambda (t: T).(\lambda (t0: TList).(\lambda (H: (eq TList (lifts h d (TApp
 173 t0 v)) (TApp (lifts h d t0) (lift h d v)))).(eq_ind_r TList (TApp (lifts h d
 174 t0) (lift h d v)) (\lambda (t1: TList).(eq TList (TCons (lift h d t) t1)
 175 (TCons (lift h d t) (TApp (lifts h d t0) (lift h d v))))) (refl_equal TList
 176 (TCons (lift h d t) (TApp (lifts h d t0) (lift h d v)))) (lifts h d (TApp t0
 177 v)) H)))) vs)))).
 178
 179 lemma lift_free:
 180  \forall (t: T).(\forall (h: nat).(\forall (k: nat).(\forall (d:
 181 nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to (eq T (lift k e
 182 (lift h d t)) (lift (plus k h) d t))))))))
 183 \def
 184  \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (h: nat).(\forall (k:
 185 nat).(\forall (d: nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to
 186 (eq T (lift k e (lift h d t0)) (lift (plus k h) d t0))))))))) (\lambda (n:
 187 nat).(\lambda (h: nat).(\lambda (k: nat).(\lambda (d: nat).(\lambda (e:
 188 nat).(\lambda (_: (le e (plus d h))).(\lambda (_: (le d e)).(eq_ind_r T
 189 (TSort n) (\lambda (t0: T).(eq T (lift k e t0) (lift (plus k h) d (TSort
 190 n)))) (eq_ind_r T (TSort n) (\lambda (t0: T).(eq T t0 (lift (plus k h) d
 191 (TSort n)))) (eq_ind_r T (TSort n) (\lambda (t0: T).(eq T (TSort n) t0))
 192 (refl_equal T (TSort n)) (lift (plus k h) d (TSort n)) (lift_sort n (plus k
 193 h) d)) (lift k e (TSort n)) (lift_sort n k e)) (lift h d (TSort n))
 194 (lift_sort n h d))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (k:
 195 nat).(\lambda (d: nat).(\lambda (e: nat).(\lambda (H: (le e (plus d
 196 h))).(\lambda (H0: (le d e)).(lt_le_e n d (eq T (lift k e (lift h d (TLRef
 197 n))) (lift (plus k h) d (TLRef n))) (\lambda (H1: (lt n d)).(eq_ind_r T
 198 (TLRef n) (\lambda (t0: T).(eq T (lift k e t0) (lift (plus k h) d (TLRef
 199 n)))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0 (lift (plus k h) d
 200 (TLRef n)))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T (TLRef n) t0))
 201 (refl_equal T (TLRef n)) (lift (plus k h) d (TLRef n)) (lift_lref_lt n (plus
 202 k h) d H1)) (lift k e (TLRef n)) (lift_lref_lt n k e (lt_le_trans n d e H1
 203 H0))) (lift h d (TLRef n)) (lift_lref_lt n h d H1))) (\lambda (H1: (le d
 204 n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0: T).(eq T (lift k e t0) (lift
 205 (plus k h) d (TLRef n)))) (eq_ind_r T (TLRef (plus (plus n h) k)) (\lambda
 206 (t0: T).(eq T t0 (lift (plus k h) d (TLRef n)))) (eq_ind_r T (TLRef (plus n
 207 (plus k h))) (\lambda (t0: T).(eq T (TLRef (plus (plus n h) k)) t0)) (f_equal
 208 nat T TLRef (plus (plus n h) k) (plus n (plus k h))
 209 (plus_permute_2_in_3_assoc n h k)) (lift (plus k h) d (TLRef n))
 210 (lift_lref_ge n (plus k h) d H1)) (lift k e (TLRef (plus n h))) (lift_lref_ge
 211 (plus n h) k e (le_trans e (plus d h) (plus n h) H (le_plus_plus d n h h H1
 212 (le_n h))))) (lift h d (TLRef n)) (lift_lref_ge n h d H1))))))))))) (\lambda
 213 (k: K).(\lambda (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (k0:
 214 nat).(\forall (d: nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to
 215 (eq T (lift k0 e (lift h d t0)) (lift (plus k0 h) d t0)))))))))).(\lambda
 216 (t1: T).(\lambda (H0: ((\forall (h: nat).(\forall (k0: nat).(\forall (d:
 217 nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to (eq T (lift k0 e
 218 (lift h d t1)) (lift (plus k0 h) d t1)))))))))).(\lambda (h: nat).(\lambda
 219 (k0: nat).(\lambda (d: nat).(\lambda (e: nat).(\lambda (H1: (le e (plus d
 220 h))).(\lambda (H2: (le d e)).(eq_ind_r T (THead k (lift h d t0) (lift h (s k
 221 d) t1)) (\lambda (t2: T).(eq T (lift k0 e t2) (lift (plus k0 h) d (THead k t0
 222 t1)))) (eq_ind_r T (THead k (lift k0 e (lift h d t0)) (lift k0 (s k e) (lift
 223 h (s k d) t1))) (\lambda (t2: T).(eq T t2 (lift (plus k0 h) d (THead k t0
 224 t1)))) (eq_ind_r T (THead k (lift (plus k0 h) d t0) (lift (plus k0 h) (s k d)
 225 t1)) (\lambda (t2: T).(eq T (THead k (lift k0 e (lift h d t0)) (lift k0 (s k
 226 e) (lift h (s k d) t1))) t2)) (f_equal3 K T T T THead k k (lift k0 e (lift h
 227 d t0)) (lift (plus k0 h) d t0) (lift k0 (s k e) (lift h (s k d) t1)) (lift
 228 (plus k0 h) (s k d) t1) (refl_equal K k) (H h k0 d e H1 H2) (H0 h k0 (s k d)
 229 (s k e) (eq_ind nat (s k (plus d h)) (\lambda (n: nat).(le (s k e) n)) (s_le
 230 k e (plus d h) H1) (plus (s k d) h) (s_plus k d h)) (s_le k d e H2))) (lift
 231 (plus k0 h) d (THead k t0 t1)) (lift_head k t0 t1 (plus k0 h) d)) (lift k0 e
 232 (THead k (lift h d t0) (lift h (s k d) t1))) (lift_head k (lift h d t0) (lift
 233 h (s k d) t1) k0 e)) (lift h d (THead k t0 t1)) (lift_head k t0 t1 h
 234 d))))))))))))) t).
 235
 236 lemma lift_free_sym:
 237  \forall (t: T).(\forall (h: nat).(\forall (k: nat).(\forall (d:
 238 nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to (eq T (lift k e
 239 (lift h d t)) (lift (plus h k) d t))))))))
 240 \def
 241  \lambda (t: T).(\lambda (h: nat).(\lambda (k: nat).(\lambda (d:
 242 nat).(\lambda (e: nat).(\lambda (H: (le e (plus d h))).(\lambda (H0: (le d
 243 e)).(eq_ind_r nat (plus k h) (\lambda (n: nat).(eq T (lift k e (lift h d t))
 244 (lift n d t))) (lift_free t h k d e H H0) (plus h k) (plus_sym h k)))))))).
 245
 246 lemma lift_d:
 247  \forall (t: T).(\forall (h: nat).(\forall (k: nat).(\forall (d:
 248 nat).(\forall (e: nat).((le e d) \to (eq T (lift h (plus k d) (lift k e t))
 249 (lift k e (lift h d t))))))))
 250 \def
 251  \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (h: nat).(\forall (k:
 252 nat).(\forall (d: nat).(\forall (e: nat).((le e d) \to (eq T (lift h (plus k
 253 d) (lift k e t0)) (lift k e (lift h d t0))))))))) (\lambda (n: nat).(\lambda
 254 (h: nat).(\lambda (k: nat).(\lambda (d: nat).(\lambda (e: nat).(\lambda (_:
 255 (le e d)).(eq_ind_r T (TSort n) (\lambda (t0: T).(eq T (lift h (plus k d) t0)
 256 (lift k e (lift h d (TSort n))))) (eq_ind_r T (TSort n) (\lambda (t0: T).(eq
 257 T t0 (lift k e (lift h d (TSort n))))) (eq_ind_r T (TSort n) (\lambda (t0:
 258 T).(eq T (TSort n) (lift k e t0))) (eq_ind_r T (TSort n) (\lambda (t0: T).(eq
 259 T (TSort n) t0)) (refl_equal T (TSort n)) (lift k e (TSort n)) (lift_sort n k
 260 e)) (lift h d (TSort n)) (lift_sort n h d)) (lift h (plus k d) (TSort n))
 261 (lift_sort n h (plus k d))) (lift k e (TSort n)) (lift_sort n k e))))))))
 262 (\lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(\lambda (d:
 263 nat).(\lambda (e: nat).(\lambda (H: (le e d)).(lt_le_e n e (eq T (lift h
 264 (plus k d) (lift k e (TLRef n))) (lift k e (lift h d (TLRef n)))) (\lambda
 265 (H0: (lt n e)).(let H1 \def (lt_le_trans n e d H0 H) in (eq_ind_r T (TLRef n)
 266 (\lambda (t0: T).(eq T (lift h (plus k d) t0) (lift k e (lift h d (TLRef
 267 n))))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0 (lift k e (lift h d
 268 (TLRef n))))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T (TLRef n) (lift k
 269 e t0))) (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T (TLRef n) t0))
 270 (refl_equal T (TLRef n)) (lift k e (TLRef n)) (lift_lref_lt n k e H0)) (lift
 271 h d (TLRef n)) (lift_lref_lt n h d H1)) (lift h (plus k d) (TLRef n))
 272 (lift_lref_lt n h (plus k d) (lt_le_trans n d (plus k d) H1 (le_plus_r k
 273 d)))) (lift k e (TLRef n)) (lift_lref_lt n k e H0)))) (\lambda (H0: (le e
 274 n)).(eq_ind_r T (TLRef (plus n k)) (\lambda (t0: T).(eq T (lift h (plus k d)
 275 t0) (lift k e (lift h d (TLRef n))))) (eq_ind_r nat (plus d k) (\lambda (n0:
 276 nat).(eq T (lift h n0 (TLRef (plus n k))) (lift k e (lift h d (TLRef n)))))
 277 (lt_le_e n d (eq T (lift h (plus d k) (TLRef (plus n k))) (lift k e (lift h d
 278 (TLRef n)))) (\lambda (H1: (lt n d)).(eq_ind_r T (TLRef (plus n k)) (\lambda
 279 (t0: T).(eq T t0 (lift k e (lift h d (TLRef n))))) (eq_ind_r T (TLRef n)
 280 (\lambda (t0: T).(eq T (TLRef (plus n k)) (lift k e t0))) (eq_ind_r T (TLRef
 281 (plus n k)) (\lambda (t0: T).(eq T (TLRef (plus n k)) t0)) (refl_equal T
 282 (TLRef (plus n k))) (lift k e (TLRef n)) (lift_lref_ge n k e H0)) (lift h d
 283 (TLRef n)) (lift_lref_lt n h d H1)) (lift h (plus d k) (TLRef (plus n k)))
 284 (lift_lref_lt (plus n k) h (plus d k) (lt_reg_r n d k H1)))) (\lambda (H1:
 285 (le d n)).(eq_ind_r T (TLRef (plus (plus n k) h)) (\lambda (t0: T).(eq T t0
 286 (lift k e (lift h d (TLRef n))))) (eq_ind_r T (TLRef (plus n h)) (\lambda
 287 (t0: T).(eq T (TLRef (plus (plus n k) h)) (lift k e t0))) (eq_ind_r T (TLRef
 288 (plus (plus n h) k)) (\lambda (t0: T).(eq T (TLRef (plus (plus n k) h)) t0))
 289 (f_equal nat T TLRef (plus (plus n k) h) (plus (plus n h) k)
 290 (plus_permute_2_in_3 n k h)) (lift k e (TLRef (plus n h))) (lift_lref_ge
 291 (plus n h) k e (le_plus_trans e n h H0))) (lift h d (TLRef n)) (lift_lref_ge
 292 n h d H1)) (lift h (plus d k) (TLRef (plus n k))) (lift_lref_ge (plus n k) h
 293 (plus d k) (le_plus_plus d n k k H1 (le_n k)))))) (plus k d) (plus_sym k d))
 294 (lift k e (TLRef n)) (lift_lref_ge n k e H0)))))))))) (\lambda (k:
 295 K).(\lambda (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (k0:
 296 nat).(\forall (d: nat).(\forall (e: nat).((le e d) \to (eq T (lift h (plus k0
 297 d) (lift k0 e t0)) (lift k0 e (lift h d t0)))))))))).(\lambda (t1:
 298 T).(\lambda (H0: ((\forall (h: nat).(\forall (k0: nat).(\forall (d:
 299 nat).(\forall (e: nat).((le e d) \to (eq T (lift h (plus k0 d) (lift k0 e
 300 t1)) (lift k0 e (lift h d t1)))))))))).(\lambda (h: nat).(\lambda (k0:
 301 nat).(\lambda (d: nat).(\lambda (e: nat).(\lambda (H1: (le e d)).(eq_ind_r T
 302 (THead k (lift k0 e t0) (lift k0 (s k e) t1)) (\lambda (t2: T).(eq T (lift h
 303 (plus k0 d) t2) (lift k0 e (lift h d (THead k t0 t1))))) (eq_ind_r T (THead k
 304 (lift h (plus k0 d) (lift k0 e t0)) (lift h (s k (plus k0 d)) (lift k0 (s k
 305 e) t1))) (\lambda (t2: T).(eq T t2 (lift k0 e (lift h d (THead k t0 t1)))))
 306 (eq_ind_r T (THead k (lift h d t0) (lift h (s k d) t1)) (\lambda (t2: T).(eq
 307 T (THead k (lift h (plus k0 d) (lift k0 e t0)) (lift h (s k (plus k0 d))
 308 (lift k0 (s k e) t1))) (lift k0 e t2))) (eq_ind_r T (THead k (lift k0 e (lift
 309 h d t0)) (lift k0 (s k e) (lift h (s k d) t1))) (\lambda (t2: T).(eq T (THead
 310 k (lift h (plus k0 d) (lift k0 e t0)) (lift h (s k (plus k0 d)) (lift k0 (s k
 311 e) t1))) t2)) (eq_ind_r nat (plus k0 (s k d)) (\lambda (n: nat).(eq T (THead
 312 k (lift h (plus k0 d) (lift k0 e t0)) (lift h n (lift k0 (s k e) t1))) (THead
 313 k (lift k0 e (lift h d t0)) (lift k0 (s k e) (lift h (s k d) t1)))))
 314 (f_equal3 K T T T THead k k (lift h (plus k0 d) (lift k0 e t0)) (lift k0 e
 315 (lift h d t0)) (lift h (plus k0 (s k d)) (lift k0 (s k e) t1)) (lift k0 (s k
 316 e) (lift h (s k d) t1)) (refl_equal K k) (H h k0 d e H1) (H0 h k0 (s k d) (s
 317 k e) (s_le k e d H1))) (s k (plus k0 d)) (s_plus_sym k k0 d)) (lift k0 e
 318 (THead k (lift h d t0) (lift h (s k d) t1))) (lift_head k (lift h d t0) (lift
 319 h (s k d) t1) k0 e)) (lift h d (THead k t0 t1)) (lift_head k t0 t1 h d))
 320 (lift h (plus k0 d) (THead k (lift k0 e t0) (lift k0 (s k e) t1))) (lift_head
 321 k (lift k0 e t0) (lift k0 (s k e) t1) h (plus k0 d))) (lift k0 e (THead k t0
 322 t1)) (lift_head k t0 t1 k0 e)))))))))))) t).
 323