helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.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/tlt".
  18
  19 include "lift/fwd.ma".
  20
  21 include "tlt/props.ma".
  22
  23 theorem lift_weight_map:
  24  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to
  25 nat))).(((\forall (m: nat).((le d m) \to (eq nat (f m) O)))) \to (eq nat
  26 (weight_map f (lift h d t)) (weight_map f t))))))
  27 \def
  28  \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (h: nat).(\forall (d:
  29 nat).(\forall (f: ((nat \to nat))).(((\forall (m: nat).((le d m) \to (eq nat
  30 (f m) O)))) \to (eq nat (weight_map f (lift h d t0)) (weight_map f t0)))))))
  31 (\lambda (n: nat).(\lambda (_: nat).(\lambda (d: nat).(\lambda (f: ((nat \to
  32 nat))).(\lambda (_: ((\forall (m: nat).((le d m) \to (eq nat (f m)
  33 O))))).(refl_equal nat (weight_map f (TSort n)))))))) (\lambda (n:
  34 nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat \to
  35 nat))).(\lambda (H: ((\forall (m: nat).((le d m) \to (eq nat (f m)
  36 O))))).(lt_le_e n d (eq nat (weight_map f (lift h d (TLRef n))) (weight_map f
  37 (TLRef n))) (\lambda (H0: (lt n d)).(eq_ind_r T (TLRef n) (\lambda (t0:
  38 T).(eq nat (weight_map f t0) (weight_map f (TLRef n)))) (refl_equal nat
  39 (weight_map f (TLRef n))) (lift h d (TLRef n)) (lift_lref_lt n h d H0)))
  40 (\lambda (H0: (le d n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0: T).(eq
  41 nat (weight_map f t0) (weight_map f (TLRef n)))) (eq_ind_r nat O (\lambda
  42 (n0: nat).(eq nat (f (plus n h)) n0)) (H (plus n h) (le_S_n d (plus n h)
  43 (le_n_S d (plus n h) (le_plus_trans d n h H0)))) (f n) (H n H0)) (lift h d
  44 (TLRef n)) (lift_lref_ge n h d H0))))))))) (\lambda (k: K).(\lambda (t0:
  45 T).(\lambda (H: ((\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to
  46 nat))).(((\forall (m: nat).((le d m) \to (eq nat (f m) O)))) \to (eq nat
  47 (weight_map f (lift h d t0)) (weight_map f t0)))))))).(\lambda (t1:
  48 T).(\lambda (H0: ((\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to
  49 nat))).(((\forall (m: nat).((le d m) \to (eq nat (f m) O)))) \to (eq nat
  50 (weight_map f (lift h d t1)) (weight_map f t1)))))))).(\lambda (h:
  51 nat).(\lambda (d: nat).(\lambda (f: ((nat \to nat))).(\lambda (H1: ((\forall
  52 (m: nat).((le d m) \to (eq nat (f m) O))))).(K_ind (\lambda (k0: K).(eq nat
  53 (weight_map f (lift h d (THead k0 t0 t1))) (weight_map f (THead k0 t0 t1))))
  54 (\lambda (b: B).(eq_ind_r T (THead (Bind b) (lift h d t0) (lift h (s (Bind b)
  55 d) t1)) (\lambda (t2: T).(eq nat (weight_map f t2) (weight_map f (THead (Bind
  56 b) t0 t1)))) (B_ind (\lambda (b0: B).(eq nat (match b0 with [Abbr \Rightarrow
  57 (S (plus (weight_map f (lift h d t0)) (weight_map (wadd f (S (weight_map f
  58 (lift h d t0)))) (lift h (S d) t1)))) | Abst \Rightarrow (S (plus (weight_map
  59 f (lift h d t0)) (weight_map (wadd f O) (lift h (S d) t1)))) | Void
  60 \Rightarrow (S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O)
  61 (lift h (S d) t1))))]) (match b0 with [Abbr \Rightarrow (S (plus (weight_map
  62 f t0) (weight_map (wadd f (S (weight_map f t0))) t1))) | Abst \Rightarrow (S
  63 (plus (weight_map f t0) (weight_map (wadd f O) t1))) | Void \Rightarrow (S
  64 (plus (weight_map f t0) (weight_map (wadd f O) t1)))]))) (eq_ind_r nat
  65 (weight_map f t0) (\lambda (n: nat).(eq nat (S (plus n (weight_map (wadd f (S
  66 n)) (lift h (S d) t1)))) (S (plus (weight_map f t0) (weight_map (wadd f (S
  67 (weight_map f t0))) t1))))) (eq_ind_r nat (weight_map (wadd f (S (weight_map
  68 f t0))) t1) (\lambda (n: nat).(eq nat (S (plus (weight_map f t0) n)) (S (plus
  69 (weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1)))))
  70 (refl_equal nat (S (plus (weight_map f t0) (weight_map (wadd f (S (weight_map
  71 f t0))) t1)))) (weight_map (wadd f (S (weight_map f t0))) (lift h (S d) t1))
  72 (H0 h (S d) (wadd f (S (weight_map f t0))) (\lambda (m: nat).(\lambda (H2:
  73 (le (S d) m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n:
  74 nat).(le d n)) (eq nat (wadd f (S (weight_map f t0)) m) O) (\lambda (x:
  75 nat).(\lambda (H3: (eq nat m (S x))).(\lambda (H4: (le d x)).(eq_ind_r nat (S
  76 x) (\lambda (n: nat).(eq nat (wadd f (S (weight_map f t0)) n) O)) (H1 x H4) m
  77 H3)))) (le_gen_S d m H2)))))) (weight_map f (lift h d t0)) (H h d f H1))
  78 (eq_ind_r nat (weight_map (wadd f O) t1) (\lambda (n: nat).(eq nat (S (plus
  79 (weight_map f (lift h d t0)) n)) (S (plus (weight_map f t0) (weight_map (wadd
  80 f O) t1))))) (f_equal nat nat S (plus (weight_map f (lift h d t0))
  81 (weight_map (wadd f O) t1)) (plus (weight_map f t0) (weight_map (wadd f O)
  82 t1)) (f_equal2 nat nat nat plus (weight_map f (lift h d t0)) (weight_map f
  83 t0) (weight_map (wadd f O) t1) (weight_map (wadd f O) t1) (H h d f H1)
  84 (refl_equal nat (weight_map (wadd f O) t1)))) (weight_map (wadd f O) (lift h
  85 (S d) t1)) (H0 h (S d) (wadd f O) (\lambda (m: nat).(\lambda (H2: (le (S d)
  86 m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d
  87 n)) (eq nat (wadd f O m) O) (\lambda (x: nat).(\lambda (H3: (eq nat m (S
  88 x))).(\lambda (H4: (le d x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat
  89 (wadd f O n) O)) (H1 x H4) m H3)))) (le_gen_S d m H2)))))) (eq_ind_r nat
  90 (weight_map (wadd f O) t1) (\lambda (n: nat).(eq nat (S (plus (weight_map f
  91 (lift h d t0)) n)) (S (plus (weight_map f t0) (weight_map (wadd f O) t1)))))
  92 (f_equal nat nat S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O)
  93 t1)) (plus (weight_map f t0) (weight_map (wadd f O) t1)) (f_equal2 nat nat
  94 nat plus (weight_map f (lift h d t0)) (weight_map f t0) (weight_map (wadd f
  95 O) t1) (weight_map (wadd f O) t1) (H h d f H1) (refl_equal nat (weight_map
  96 (wadd f O) t1)))) (weight_map (wadd f O) (lift h (S d) t1)) (H0 h (S d) (wadd
  97 f O) (\lambda (m: nat).(\lambda (H2: (le (S d) m)).(ex2_ind nat (\lambda (n:
  98 nat).(eq nat m (S n))) (\lambda (n: nat).(le d n)) (eq nat (wadd f O m) O)
  99 (\lambda (x: nat).(\lambda (H3: (eq nat m (S x))).(\lambda (H4: (le d
 100 x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (wadd f O n) O)) (H1 x H4)
 101 m H3)))) (le_gen_S d m H2)))))) b) (lift h d (THead (Bind b) t0 t1))
 102 (lift_head (Bind b) t0 t1 h d))) (\lambda (f0: F).(eq_ind_r T (THead (Flat
 103 f0) (lift h d t0) (lift h (s (Flat f0) d) t1)) (\lambda (t2: T).(eq nat
 104 (weight_map f t2) (weight_map f (THead (Flat f0) t0 t1)))) (f_equal nat nat S
 105 (plus (weight_map f (lift h d t0)) (weight_map f (lift h d t1))) (plus
 106 (weight_map f t0) (weight_map f t1)) (f_equal2 nat nat nat plus (weight_map f
 107 (lift h d t0)) (weight_map f t0) (weight_map f (lift h d t1)) (weight_map f
 108 t1) (H h d f H1) (H0 h d f H1))) (lift h d (THead (Flat f0) t0 t1))
 109 (lift_head (Flat f0) t0 t1 h d))) k)))))))))) t).
 110
 111 theorem lift_weight:
 112  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(eq nat (weight (lift h d
 113 t)) (weight t))))
 114 \def
 115  \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(lift_weight_map t h d
 116 (\lambda (_: nat).O) (\lambda (m: nat).(\lambda (_: (le d m)).(refl_equal nat
 117 O)))))).
 118
 119 theorem lift_weight_add:
 120  \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (d:
 121 nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
 122 (m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to
 123 (((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m))))) \to (eq nat
 124 (weight_map f (lift h d t)) (weight_map g (lift (S h) d t)))))))))))
 125 \def
 126  \lambda (w: nat).(\lambda (t: T).(T_ind (\lambda (t0: T).(\forall (h:
 127 nat).(\forall (d: nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 128 nat))).(((\forall (m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat
 129 (g d) w) \to (((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m)))))
 130 \to (eq nat (weight_map f (lift h d t0)) (weight_map g (lift (S h) d
 131 t0))))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda
 132 (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall (m:
 133 nat).((lt m d) \to (eq nat (g m) (f m)))))).(\lambda (_: (eq nat (g d)
 134 w)).(\lambda (_: ((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f
 135 m)))))).(refl_equal nat (weight_map g (lift (S h) d (TSort n))))))))))))
 136 (\lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat \to
 137 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H: ((\forall (m: nat).((lt m
 138 d) \to (eq nat (g m) (f m)))))).(\lambda (_: (eq nat (g d) w)).(\lambda (H1:
 139 ((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f m)))))).(lt_le_e n d
 140 (eq nat (weight_map f (lift h d (TLRef n))) (weight_map g (lift (S h) d
 141 (TLRef n)))) (\lambda (H2: (lt n d)).(eq_ind_r T (TLRef n) (\lambda (t0:
 142 T).(eq nat (weight_map f t0) (weight_map g (lift (S h) d (TLRef n)))))
 143 (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq nat (weight_map f (TLRef n))
 144 (weight_map g t0))) (sym_equal nat (g n) (f n) (H n H2)) (lift (S h) d (TLRef
 145 n)) (lift_lref_lt n (S h) d H2)) (lift h d (TLRef n)) (lift_lref_lt n h d
 146 H2))) (\lambda (H2: (le d n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0:
 147 T).(eq nat (weight_map f t0) (weight_map g (lift (S h) d (TLRef n)))))
 148 (eq_ind_r T (TLRef (plus n (S h))) (\lambda (t0: T).(eq nat (weight_map f
 149 (TLRef (plus n h))) (weight_map g t0))) (eq_ind nat (S (plus n h)) (\lambda
 150 (n0: nat).(eq nat (f (plus n h)) (g n0))) (sym_equal nat (g (S (plus n h)))
 151 (f (plus n h)) (H1 (plus n h) (le_plus_trans d n h H2))) (plus n (S h))
 152 (plus_n_Sm n h)) (lift (S h) d (TLRef n)) (lift_lref_ge n (S h) d H2)) (lift
 153 h d (TLRef n)) (lift_lref_ge n h d H2)))))))))))) (\lambda (k: K).(\lambda
 154 (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat
 155 \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).((lt m d) \to
 156 (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to (((\forall (m: nat).((le d
 157 m) \to (eq nat (g (S m)) (f m))))) \to (eq nat (weight_map f (lift h d t0))
 158 (weight_map g (lift (S h) d t0)))))))))))).(\lambda (t1: T).(\lambda (H0:
 159 ((\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to nat))).(\forall
 160 (g: ((nat \to nat))).(((\forall (m: nat).((lt m d) \to (eq nat (g m) (f
 161 m))))) \to ((eq nat (g d) w) \to (((\forall (m: nat).((le d m) \to (eq nat (g
 162 (S m)) (f m))))) \to (eq nat (weight_map f (lift h d t1)) (weight_map g (lift
 163 (S h) d t1)))))))))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (f: ((nat
 164 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (m:
 165 nat).((lt m d) \to (eq nat (g m) (f m)))))).(\lambda (H2: (eq nat (g d)
 166 w)).(\lambda (H3: ((\forall (m: nat).((le d m) \to (eq nat (g (S m)) (f
 167 m)))))).(K_ind (\lambda (k0: K).(eq nat (weight_map f (lift h d (THead k0 t0
 168 t1))) (weight_map g (lift (S h) d (THead k0 t0 t1))))) (\lambda (b:
 169 B).(eq_ind_r T (THead (Bind b) (lift h d t0) (lift h (s (Bind b) d) t1))
 170 (\lambda (t2: T).(eq nat (weight_map f t2) (weight_map g (lift (S h) d (THead
 171 (Bind b) t0 t1))))) (eq_ind_r T (THead (Bind b) (lift (S h) d t0) (lift (S h)
 172 (s (Bind b) d) t1)) (\lambda (t2: T).(eq nat (weight_map f (THead (Bind b)
 173 (lift h d t0) (lift h (s (Bind b) d) t1))) (weight_map g t2))) (B_ind
 174 (\lambda (b0: B).(eq nat (match b0 with [Abbr \Rightarrow (S (plus
 175 (weight_map f (lift h d t0)) (weight_map (wadd f (S (weight_map f (lift h d
 176 t0)))) (lift h (S d) t1)))) | Abst \Rightarrow (S (plus (weight_map f (lift h
 177 d t0)) (weight_map (wadd f O) (lift h (S d) t1)))) | Void \Rightarrow (S
 178 (plus (weight_map f (lift h d t0)) (weight_map (wadd f O) (lift h (S d)
 179 t1))))]) (match b0 with [Abbr \Rightarrow (S (plus (weight_map g (lift (S h)
 180 d t0)) (weight_map (wadd g (S (weight_map g (lift (S h) d t0)))) (lift (S h)
 181 (S d) t1)))) | Abst \Rightarrow (S (plus (weight_map g (lift (S h) d t0))
 182 (weight_map (wadd g O) (lift (S h) (S d) t1)))) | Void \Rightarrow (S (plus
 183 (weight_map g (lift (S h) d t0)) (weight_map (wadd g O) (lift (S h) (S d)
 184 t1))))]))) (f_equal nat nat S (plus (weight_map f (lift h d t0)) (weight_map
 185 (wadd f (S (weight_map f (lift h d t0)))) (lift h (S d) t1))) (plus
 186 (weight_map g (lift (S h) d t0)) (weight_map (wadd g (S (weight_map g (lift
 187 (S h) d t0)))) (lift (S h) (S d) t1))) (f_equal2 nat nat nat plus (weight_map
 188 f (lift h d t0)) (weight_map g (lift (S h) d t0)) (weight_map (wadd f (S
 189 (weight_map f (lift h d t0)))) (lift h (S d) t1)) (weight_map (wadd g (S
 190 (weight_map g (lift (S h) d t0)))) (lift (S h) (S d) t1)) (H h d f g H1 H2
 191 H3) (H0 h (S d) (wadd f (S (weight_map f (lift h d t0)))) (wadd g (S
 192 (weight_map g (lift (S h) d t0)))) (\lambda (m: nat).(\lambda (H4: (lt m (S
 193 d))).(or_ind (eq nat m O) (ex2 nat (\lambda (m0: nat).(eq nat m (S m0)))
 194 (\lambda (m0: nat).(lt m0 d))) (eq nat (wadd g (S (weight_map g (lift (S h) d
 195 t0))) m) (wadd f (S (weight_map f (lift h d t0))) m)) (\lambda (H5: (eq nat m
 196 O)).(eq_ind_r nat O (\lambda (n: nat).(eq nat (wadd g (S (weight_map g (lift
 197 (S h) d t0))) n) (wadd f (S (weight_map f (lift h d t0))) n))) (f_equal nat
 198 nat S (weight_map g (lift (S h) d t0)) (weight_map f (lift h d t0))
 199 (sym_equal nat (weight_map f (lift h d t0)) (weight_map g (lift (S h) d t0))
 200 (H h d f g H1 H2 H3))) m H5)) (\lambda (H5: (ex2 nat (\lambda (m0: nat).(eq
 201 nat m (S m0))) (\lambda (m: nat).(lt m d)))).(ex2_ind nat (\lambda (m0:
 202 nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)) (eq nat (wadd g (S
 203 (weight_map g (lift (S h) d t0))) m) (wadd f (S (weight_map f (lift h d t0)))
 204 m)) (\lambda (x: nat).(\lambda (H6: (eq nat m (S x))).(\lambda (H7: (lt x
 205 d)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (wadd g (S (weight_map g
 206 (lift (S h) d t0))) n) (wadd f (S (weight_map f (lift h d t0))) n))) (H1 x
 207 H7) m H6)))) H5)) (lt_gen_xS m d H4)))) H2 (\lambda (m: nat).(\lambda (H4:
 208 (le (S d) m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n:
 209 nat).(le d n)) (eq nat (g m) (wadd f (S (weight_map f (lift h d t0))) m))
 210 (\lambda (x: nat).(\lambda (H5: (eq nat m (S x))).(\lambda (H6: (le d
 211 x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (g n) (wadd f (S
 212 (weight_map f (lift h d t0))) n))) (H3 x H6) m H5)))) (le_gen_S d m H4)))))))
 213 (f_equal nat nat S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O)
 214 (lift h (S d) t1))) (plus (weight_map g (lift (S h) d t0)) (weight_map (wadd
 215 g O) (lift (S h) (S d) t1))) (f_equal2 nat nat nat plus (weight_map f (lift h
 216 d t0)) (weight_map g (lift (S h) d t0)) (weight_map (wadd f O) (lift h (S d)
 217 t1)) (weight_map (wadd g O) (lift (S h) (S d) t1)) (H h d f g H1 H2 H3) (H0 h
 218 (S d) (wadd f O) (wadd g O) (\lambda (m: nat).(\lambda (H4: (lt m (S
 219 d))).(or_ind (eq nat m O) (ex2 nat (\lambda (m0: nat).(eq nat m (S m0)))
 220 (\lambda (m0: nat).(lt m0 d))) (eq nat (wadd g O m) (wadd f O m)) (\lambda
 221 (H5: (eq nat m O)).(eq_ind_r nat O (\lambda (n: nat).(eq nat (wadd g O n)
 222 (wadd f O n))) (refl_equal nat O) m H5)) (\lambda (H5: (ex2 nat (\lambda (m0:
 223 nat).(eq nat m (S m0))) (\lambda (m: nat).(lt m d)))).(ex2_ind nat (\lambda
 224 (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)) (eq nat (wadd g O
 225 m) (wadd f O m)) (\lambda (x: nat).(\lambda (H6: (eq nat m (S x))).(\lambda
 226 (H7: (lt x d)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (wadd g O n)
 227 (wadd f O n))) (H1 x H7) m H6)))) H5)) (lt_gen_xS m d H4)))) H2 (\lambda (m:
 228 nat).(\lambda (H4: (le (S d) m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S
 229 n))) (\lambda (n: nat).(le d n)) (eq nat (g m) (wadd f O m)) (\lambda (x:
 230 nat).(\lambda (H5: (eq nat m (S x))).(\lambda (H6: (le d x)).(eq_ind_r nat (S
 231 x) (\lambda (n: nat).(eq nat (g n) (wadd f O n))) (H3 x H6) m H5))))
 232 (le_gen_S d m H4))))))) (f_equal nat nat S (plus (weight_map f (lift h d t0))
 233 (weight_map (wadd f O) (lift h (S d) t1))) (plus (weight_map g (lift (S h) d
 234 t0)) (weight_map (wadd g O) (lift (S h) (S d) t1))) (f_equal2 nat nat nat
 235 plus (weight_map f (lift h d t0)) (weight_map g (lift (S h) d t0))
 236 (weight_map (wadd f O) (lift h (S d) t1)) (weight_map (wadd g O) (lift (S h)
 237 (S d) t1)) (H h d f g H1 H2 H3) (H0 h (S d) (wadd f O) (wadd g O) (\lambda
 238 (m: nat).(\lambda (H4: (lt m (S d))).(or_ind (eq nat m O) (ex2 nat (\lambda
 239 (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d))) (eq nat (wadd g O
 240 m) (wadd f O m)) (\lambda (H5: (eq nat m O)).(eq_ind_r nat O (\lambda (n:
 241 nat).(eq nat (wadd g O n) (wadd f O n))) (refl_equal nat O) m H5)) (\lambda
 242 (H5: (ex2 nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m: nat).(lt m
 243 d)))).(ex2_ind nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m0:
 244 nat).(lt m0 d)) (eq nat (wadd g O m) (wadd f O m)) (\lambda (x: nat).(\lambda
 245 (H6: (eq nat m (S x))).(\lambda (H7: (lt x d)).(eq_ind_r nat (S x) (\lambda
 246 (n: nat).(eq nat (wadd g O n) (wadd f O n))) (H1 x H7) m H6)))) H5))
 247 (lt_gen_xS m d H4)))) H2 (\lambda (m: nat).(\lambda (H4: (le (S d)
 248 m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d
 249 n)) (eq nat (g m) (wadd f O m)) (\lambda (x: nat).(\lambda (H5: (eq nat m (S
 250 x))).(\lambda (H6: (le d x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (g
 251 n) (wadd f O n))) (H3 x H6) m H5)))) (le_gen_S d m H4))))))) b) (lift (S h) d
 252 (THead (Bind b) t0 t1)) (lift_head (Bind b) t0 t1 (S h) d)) (lift h d (THead
 253 (Bind b) t0 t1)) (lift_head (Bind b) t0 t1 h d))) (\lambda (f0: F).(eq_ind_r
 254 T (THead (Flat f0) (lift h d t0) (lift h (s (Flat f0) d) t1)) (\lambda (t2:
 255 T).(eq nat (weight_map f t2) (weight_map g (lift (S h) d (THead (Flat f0) t0
 256 t1))))) (eq_ind_r T (THead (Flat f0) (lift (S h) d t0) (lift (S h) (s (Flat
 257 f0) d) t1)) (\lambda (t2: T).(eq nat (weight_map f (THead (Flat f0) (lift h d
 258 t0) (lift h (s (Flat f0) d) t1))) (weight_map g t2))) (f_equal nat nat S
 259 (plus (weight_map f (lift h d t0)) (weight_map f (lift h d t1))) (plus
 260 (weight_map g (lift (S h) d t0)) (weight_map g (lift (S h) d t1))) (f_equal2
 261 nat nat nat plus (weight_map f (lift h d t0)) (weight_map g (lift (S h) d
 262 t0)) (weight_map f (lift h d t1)) (weight_map g (lift (S h) d t1)) (H h d f g
 263 H1 H2 H3) (H0 h d f g H1 H2 H3))) (lift (S h) d (THead (Flat f0) t0 t1))
 264 (lift_head (Flat f0) t0 t1 (S h) d)) (lift h d (THead (Flat f0) t0 t1))
 265 (lift_head (Flat f0) t0 t1 h d))) k))))))))))))) t)).
 266
 267 theorem lift_weight_add_O:
 268  \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (f: ((nat \to
 269 nat))).(eq nat (weight_map f (lift h O t)) (weight_map (wadd f w) (lift (S h)
 270 O t))))))
 271 \def
 272  \lambda (w: nat).(\lambda (t: T).(\lambda (h: nat).(\lambda (f: ((nat \to
 273 nat))).(lift_weight_add (plus (wadd f w O) O) t h O f (wadd f w) (\lambda (m:
 274 nat).(\lambda (H: (lt m O)).(let H0 \def (match H in le return (\lambda (n:
 275 nat).(\lambda (_: (le ? n)).((eq nat n O) \to (eq nat (wadd f w m) (f m)))))
 276 with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) O)).(let H1 \def (eq_ind
 277 nat (S m) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop)
 278 with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind
 279 (eq nat (wadd f w m) (f m)) H1))) | (le_S m0 H0) \Rightarrow (\lambda (H1:
 280 (eq nat (S m0) O)).((let H2 \def (eq_ind nat (S m0) (\lambda (e: nat).(match
 281 e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
 282 \Rightarrow True])) I O H1) in (False_ind ((le (S m) m0) \to (eq nat (wadd f
 283 w m) (f m))) H2)) H0))]) in (H0 (refl_equal nat O))))) (plus_n_O (wadd f w
 284 O)) (\lambda (m: nat).(\lambda (_: (le O m)).(refl_equal nat (f m)))))))).
 285
 286 theorem lift_tlt_dx:
 287  \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall
 288 (d: nat).(tlt t (THead k u (lift h d t)))))))
 289 \def
 290  \lambda (k: K).(\lambda (u: T).(\lambda (t: T).(\lambda (h: nat).(\lambda
 291 (d: nat).(eq_ind nat (weight (lift h d t)) (\lambda (n: nat).(lt n (weight
 292 (THead k u (lift h d t))))) (tlt_head_dx k u (lift h d t)) (weight t)
 293 (lift_weight t h d)))))).
 294