matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/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/LambdaDelta-1/subst0/tlt".
  18
  19 include "subst0/defs.ma".
  20
  21 include "lift/props.ma".
  22
  23 include "lift/tlt.ma".
  24
  25 theorem subst0_weight_le:
  26  \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
  27 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
  28 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
  29 d) O u)) (g d)) \to (le (weight_map f z) (weight_map g t))))))))))
  30 \def
  31  \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
  32 (H: (subst0 d u t z)).(subst0_ind (\lambda (n: nat).(\lambda (t0: T).(\lambda
  33 (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
  34 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
  35 n) O t0)) (g n)) \to (le (weight_map f t2) (weight_map g t1))))))))))
  36 (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to nat))).(\lambda (g:
  37 ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f m) (g m))))).(\lambda
  38 (H1: (lt (weight_map f (lift (S i) O v)) (g i))).(le_S_n (weight_map f (lift
  39 (S i) O v)) (weight_map g (TLRef i)) (le_S (S (weight_map f (lift (S i) O
  40 v))) (weight_map g (TLRef i)) H1)))))))) (\lambda (v: T).(\lambda (u2:
  41 T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v u1
  42 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
  43 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
  44 i) O v)) (g i)) \to (le (weight_map f u2) (weight_map g u1)))))))).(\lambda
  45 (t0: T).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (f: ((nat \to
  46 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
  47 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead
  48 k0 u2 t0)) (weight_map g (THead k0 u1 t0)))))))) (\lambda (b: B).(B_ind
  49 (\lambda (b0: B).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
  50 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
  51 i) O v)) (g i)) \to (le (weight_map f (THead (Bind b0) u2 t0)) (weight_map g
  52 (THead (Bind b0) u1 t0)))))))) (\lambda (f: ((nat \to nat))).(\lambda (g:
  53 ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g
  54 m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(le_n_S
  55 (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f u2))) t0)) (plus
  56 (weight_map g u1) (weight_map (wadd g (S (weight_map g u1))) t0))
  57 (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S
  58 (weight_map f u2))) t0) (weight_map (wadd g (S (weight_map g u1))) t0) (H1 f
  59 g H2 H3) (weight_le t0 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map
  60 g u1))) (\lambda (n: nat).(wadd_le f g H2 (S (weight_map f u2)) (S
  61 (weight_map g u1)) (le_n_S (weight_map f u2) (weight_map g u1) (H1 f g H2
  62 H3)) n))))))))) (\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
  63 nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt
  64 (weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u2)
  65 (weight_map (wadd f O) t0)) (plus (weight_map g u1) (weight_map (wadd g O)
  66 t0)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
  67 O) t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O)
  68 (wadd g O) (\lambda (n: nat).(wadd_le f g H2 O O (le_n O) n))))))))) (\lambda
  69 (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall
  70 (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O
  71 v)) (g i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f O) t0)) (plus
  72 (weight_map g u1) (weight_map (wadd g O) t0)) (plus_le_compat (weight_map f
  73 u2) (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
  74 (H1 f g H2 H3) (weight_le t0 (wadd f O) (wadd g O) (\lambda (n: nat).(wadd_le
  75 f g H2 O O (le_n O) n))))))))) b)) (\lambda (_: F).(\lambda (f0: ((nat \to
  76 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0
  77 m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v)) (g
  78 i))).(lt_le_S (plus (weight_map f0 u2) (weight_map f0 t0)) (S (plus
  79 (weight_map g u1) (weight_map g t0))) (le_lt_n_Sm (plus (weight_map f0 u2)
  80 (weight_map f0 t0)) (plus (weight_map g u1) (weight_map g t0))
  81 (plus_le_compat (weight_map f0 u2) (weight_map g u1) (weight_map f0 t0)
  82 (weight_map g t0) (H1 f0 g H2 H3) (weight_le t0 f0 g H2))))))))) k)))))))))
  83 (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (v: T).(\forall (t2:
  84 T).(\forall (t1: T).(\forall (i: nat).((subst0 (s k0 i) v t1 t2) \to
  85 (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
  86 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s
  87 k0 i))) \to (le (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0:
  88 T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
  89 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to
  90 (le (weight_map f (THead k0 u0 t2)) (weight_map g (THead k0 u0
  91 t1))))))))))))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (v:
  92 T).(\forall (t2: T).(\forall (t1: T).(\forall (i: nat).((subst0 (s (Bind b0)
  93 i) v t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
  94 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
  95 (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (le (weight_map f t2)
  96 (weight_map g t1))))))) \to (\forall (u0: T).(\forall (f: ((nat \to
  97 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
  98 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead
  99 (Bind b0) u0 t2)) (weight_map g (THead (Bind b0) u0 t1)))))))))))))))
 100 (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
 101 (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to
 102 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
 103 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le (weight_map f
 104 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to
 105 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f
 106 m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
 107 i))).(le_n_S (plus (weight_map f u0) (weight_map (wadd f (S (weight_map f
 108 u0))) t2)) (plus (weight_map g u0) (weight_map (wadd g (S (weight_map g u0)))
 109 t1)) (plus_le_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd f
 110 (S (weight_map f u0))) t2) (weight_map (wadd g (S (weight_map g u0))) t1)
 111 (weight_le u0 f g H2) (H1 (wadd f (S (weight_map f u0))) (wadd g (S
 112 (weight_map g u0))) (\lambda (m: nat).(wadd_le f g H2 (S (weight_map f u0))
 113 (S (weight_map g u0)) (le_n_S (weight_map f u0) (weight_map g u0) (weight_le
 114 u0 f g H2)) m)) (lt_le_S (weight_map (wadd f (S (weight_map f u0))) (lift (S
 115 (S i)) O v)) (wadd g (S (weight_map g u0)) (S i)) (eq_ind nat (weight_map f
 116 (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3 (weight_map (wadd f (S
 117 (weight_map f u0))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f
 118 u0)) v (S i) f))))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda
 119 (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1:
 120 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
 121 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
 122 i))) \to (le (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0:
 123 T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2:
 124 ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift
 125 (S i) O v)) (g i))).(le_n_S (plus (weight_map f u0) (weight_map (wadd f O)
 126 t2)) (plus (weight_map g u0) (weight_map (wadd g O) t1)) (plus_le_compat
 127 (weight_map f u0) (weight_map g u0) (weight_map (wadd f O) t2) (weight_map
 128 (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O) (wadd g O) (\lambda (m:
 129 nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O
 130 v)) (\lambda (n: nat).(lt n (g i))) H3 (weight_map (wadd f O) (lift (S (S i))
 131 O v)) (lift_weight_add_O O v (S i) f)))))))))))))))) (\lambda (v: T).(\lambda
 132 (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1
 133 t2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 134 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 135 (S i)) O v)) (g (S i))) \to (le (weight_map f t2) (weight_map g
 136 t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
 137 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3:
 138 (lt (weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u0)
 139 (weight_map (wadd f O) t2)) (plus (weight_map g u0) (weight_map (wadd g O)
 140 t1)) (plus_le_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd f
 141 O) t2) (weight_map (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O) (wadd
 142 g O) (\lambda (m: nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat
 143 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3
 144 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v (S i)
 145 f)))))))))))))))) b)) (\lambda (_: F).(\lambda (v: T).(\lambda (t2:
 146 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v t1
 147 t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
 148 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
 149 (S i) O v)) (g i)) \to (le (weight_map f0 t2) (weight_map g
 150 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
 151 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
 152 (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_le_S (plus (weight_map
 153 f0 u0) (weight_map f0 t2)) (S (plus (weight_map g u0) (weight_map g t1)))
 154 (le_lt_n_Sm (plus (weight_map f0 u0) (weight_map f0 t2)) (plus (weight_map g
 155 u0) (weight_map g t1)) (plus_le_compat (weight_map f0 u0) (weight_map g u0)
 156 (weight_map f0 t2) (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2
 157 H3)))))))))))))))) k)) (\lambda (v: T).(\lambda (u1: T).(\lambda (u2:
 158 T).(\lambda (i: nat).(\lambda (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall
 159 (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f
 160 m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le
 161 (weight_map f u2) (weight_map g u1)))))))).(\lambda (k: K).(K_ind (\lambda
 162 (k0: K).(\forall (t1: T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to
 163 (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
 164 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s
 165 k0 i))) \to (le (weight_map f t2) (weight_map g t1))))))) \to (\forall (f:
 166 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
 167 (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map
 168 f (THead k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b:
 169 B).(B_ind (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s
 170 (Bind b0) i) v t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat
 171 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f
 172 (lift (S (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (le (weight_map f
 173 t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g:
 174 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
 175 f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead (Bind b0) u2 t2))
 176 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda
 177 (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f:
 178 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
 179 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le
 180 (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to
 181 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f
 182 m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
 183 i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f
 184 u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
 185 t1)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
 186 (S (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1) (H1
 187 f g H4 H5) (H3 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map g u1)))
 188 (\lambda (m: nat).(wadd_le f g H4 (S (weight_map f u2)) (S (weight_map g u1))
 189 (le_n_S (weight_map f u2) (weight_map g u1) (H1 f g H4 H5)) m)) (lt_le_S
 190 (weight_map (wadd f (S (weight_map f u2))) (lift (S (S i)) O v)) (wadd g (S
 191 (weight_map g u1)) (S i)) (eq_ind nat (weight_map f (lift (S i) O v))
 192 (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f (S (weight_map f u2)))
 193 (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f u2)) v (S i)
 194 f)))))))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i)
 195 v t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 196 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 197 (S i)) O v)) (g (S i))) \to (le (weight_map f t2) (weight_map g
 198 t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
 199 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt
 200 (weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u2)
 201 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O)
 202 t1)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
 203 O) t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O)
 204 (\lambda (m: nat).(wadd_le f g H4 O O (le_n O) m)) (eq_ind nat (weight_map f
 205 (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O)
 206 (lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) (\lambda
 207 (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
 208 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
 209 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
 210 i))) \to (le (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
 211 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
 212 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
 213 i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
 214 (weight_map g u1) (weight_map (wadd g O) t1)) (plus_le_compat (weight_map f
 215 u2) (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
 216 (H1 f g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f g H4 O
 217 O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n:
 218 nat).(lt n (g i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v))
 219 (lift_weight_add_O O v (S i) f))))))))))))) b)) (\lambda (_: F).(\lambda (t1:
 220 T).(\lambda (t2: T).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H3: ((\forall
 221 (f0: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le
 222 (f0 m) (g m)))) \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (le
 223 (weight_map f0 t2) (weight_map g t1)))))))).(\lambda (f0: ((nat \to
 224 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f0
 225 m) (g m))))).(\lambda (H5: (lt (weight_map f0 (lift (S i) O v)) (g
 226 i))).(lt_le_S (plus (weight_map f0 u2) (weight_map f0 t2)) (S (plus
 227 (weight_map g u1) (weight_map g t1))) (le_lt_n_Sm (plus (weight_map f0 u2)
 228 (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1))
 229 (plus_le_compat (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2)
 230 (weight_map g t1) (H1 f0 g H4 H5) (H3 f0 g H4 H5))))))))))))) k)))))))) d u t
 231 z H))))).
 232
 233 theorem subst0_weight_lt:
 234  \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
 235 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 236 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 237 d) O u)) (g d)) \to (lt (weight_map f z) (weight_map g t))))))))))
 238 \def
 239  \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
 240 (H: (subst0 d u t z)).(subst0_ind (\lambda (n: nat).(\lambda (t0: T).(\lambda
 241 (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 242 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 243 n) O t0)) (g n)) \to (lt (weight_map f t2) (weight_map g t1))))))))))
 244 (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to nat))).(\lambda (g:
 245 ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f m) (g m))))).(\lambda
 246 (H1: (lt (weight_map f (lift (S i) O v)) (g i))).H1)))))) (\lambda (v:
 247 T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i
 248 v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 249 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 250 i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map g u1)))))))).(\lambda
 251 (t0: T).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (f: ((nat \to
 252 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
 253 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
 254 k0 u2 t0)) (weight_map g (THead k0 u1 t0)))))))) (\lambda (b: B).(B_ind
 255 (\lambda (b0: B).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 256 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 257 i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t0)) (weight_map g
 258 (THead (Bind b0) u1 t0)))))))) (\lambda (f: ((nat \to nat))).(\lambda (g:
 259 ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g
 260 m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S
 261 (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f u2))) t0)) (plus
 262 (weight_map g u1) (weight_map (wadd g (S (weight_map g u1))) t0))
 263 (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S
 264 (weight_map f u2))) t0) (weight_map (wadd g (S (weight_map g u1))) t0) (H1 f
 265 g H2 H3) (weight_le t0 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map
 266 g u1))) (\lambda (n: nat).(wadd_le f g H2 (S (weight_map f u2)) (S
 267 (weight_map g u1)) (le_S (S (weight_map f u2)) (weight_map g u1) (lt_le_S
 268 (weight_map f u2) (weight_map g u1) (H1 f g H2 H3))) n))))))))) (\lambda (f:
 269 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
 270 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
 271 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t0)) (plus
 272 (weight_map g u1) (weight_map (wadd g O) t0)) (plus_lt_le_compat (weight_map
 273 f u2) (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
 274 (H1 f g H2 H3) (weight_le t0 (wadd f O) (wadd g O) (\lambda (n: nat).(le_S_n
 275 (wadd f O n) (wadd g O n) (le_n_S (wadd f O n) (wadd g O n) (wadd_le f g H2 O
 276 O (le_n O) n))))))))))) (\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
 277 nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt
 278 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
 279 (weight_map (wadd f O) t0)) (plus (weight_map g u1) (weight_map (wadd g O)
 280 t0)) (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd
 281 f O) t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O)
 282 (wadd g O) (\lambda (n: nat).(le_S_n (wadd f O n) (wadd g O n) (le_n_S (wadd
 283 f O n) (wadd g O n) (wadd_le f g H2 O O (le_n O) n))))))))))) b)) (\lambda
 284 (_: F).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda
 285 (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda (H3: (lt (weight_map f0
 286 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f0 u2) (weight_map f0
 287 t0)) (plus (weight_map g u1) (weight_map g t0)) (plus_lt_le_compat
 288 (weight_map f0 u2) (weight_map g u1) (weight_map f0 t0) (weight_map g t0) (H1
 289 f0 g H2 H3) (weight_le t0 f0 g H2)))))))) k))))))))) (\lambda (k: K).(K_ind
 290 (\lambda (k0: K).(\forall (v: T).(\forall (t2: T).(\forall (t1: T).(\forall
 291 (i: nat).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to
 292 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
 293 \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (lt
 294 (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0: T).(\forall (f:
 295 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
 296 (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map
 297 f (THead k0 u0 t2)) (weight_map g (THead k0 u0 t1))))))))))))))) (\lambda (b:
 298 B).(B_ind (\lambda (b0: B).(\forall (v: T).(\forall (t2: T).(\forall (t1:
 299 T).(\forall (i: nat).((subst0 (s (Bind b0) i) v t1 t2) \to (((\forall (f:
 300 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
 301 (g m)))) \to ((lt (weight_map f (lift (S (s (Bind b0) i)) O v)) (g (s (Bind
 302 b0) i))) \to (lt (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0:
 303 T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
 304 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to
 305 (lt (weight_map f (THead (Bind b0) u0 t2)) (weight_map g (THead (Bind b0) u0
 306 t1))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda
 307 (i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f:
 308 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
 309 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
 310 (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f:
 311 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
 312 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
 313 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f (S (weight_map f
 314 u0))) t2)) (plus (weight_map g u0) (weight_map (wadd g (S (weight_map g u0)))
 315 t1)) (plus_le_lt_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd
 316 f (S (weight_map f u0))) t2) (weight_map (wadd g (S (weight_map g u0))) t1)
 317 (weight_le u0 f g H2) (H1 (wadd f (S (weight_map f u0))) (wadd g (S
 318 (weight_map g u0))) (\lambda (m: nat).(wadd_le f g H2 (S (weight_map f u0))
 319 (S (weight_map g u0)) (lt_le_S (weight_map f u0) (S (weight_map g u0))
 320 (le_lt_n_Sm (weight_map f u0) (weight_map g u0) (weight_le u0 f g H2))) m))
 321 (lt_le_S (weight_map (wadd f (S (weight_map f u0))) (lift (S (S i)) O v))
 322 (wadd g (S (weight_map g u0)) (S i)) (eq_ind nat (weight_map f (lift (S i) O
 323 v)) (\lambda (n: nat).(lt n (g i))) H3 (weight_map (wadd f (S (weight_map f
 324 u0))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f u0)) v (S i)
 325 f))))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda
 326 (i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f:
 327 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
 328 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
 329 (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f:
 330 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
 331 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
 332 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f O) t2)) (plus
 333 (weight_map g u0) (weight_map (wadd g O) t1)) (plus_le_lt_compat (weight_map
 334 f u0) (weight_map g u0) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
 335 (weight_le u0 f g H2) (H1 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f
 336 g H2 O O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda
 337 (n: nat).(lt n (g i))) H3 (weight_map (wadd f O) (lift (S (S i)) O v))
 338 (lift_weight_add_O O v (S i) f)))))))))))))))) (\lambda (v: T).(\lambda (t2:
 339 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1
 340 t2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 341 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 342 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
 343 t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
 344 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3:
 345 (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u0)
 346 (weight_map (wadd f O) t2)) (plus (weight_map g u0) (weight_map (wadd g O)
 347 t1)) (plus_le_lt_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd
 348 f O) t2) (weight_map (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O)
 349 (wadd g O) (\lambda (m: nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat
 350 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3
 351 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v (S i)
 352 f)))))))))))))))) b)) (\lambda (_: F).(\lambda (v: T).(\lambda (t2:
 353 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v t1
 354 t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
 355 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
 356 (S i) O v)) (g i)) \to (lt (weight_map f0 t2) (weight_map g
 357 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
 358 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
 359 (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
 360 f0 u0) (weight_map f0 t2)) (plus (weight_map g u0) (weight_map g t1))
 361 (plus_le_lt_compat (weight_map f0 u0) (weight_map g u0) (weight_map f0 t2)
 362 (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2 H3))))))))))))))) k))
 363 (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda
 364 (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall
 365 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
 366 (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map
 367 g u1)))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t1:
 368 T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to
 369 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
 370 \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (lt
 371 (weight_map f t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to
 372 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
 373 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
 374 k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b: B).(B_ind
 375 (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s (Bind b0) i) v
 376 t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 377 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 378 (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (lt (weight_map f t2)
 379 (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat
 380 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f
 381 (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t2))
 382 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda
 383 (t2: T).(\lambda (H2: (subst0 (S i) v t1 t2)).(\lambda (_: ((\forall (f:
 384 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
 385 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
 386 (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to
 387 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f
 388 m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
 389 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f
 390 u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
 391 t1)) (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd
 392 f (S (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1)
 393 (H1 f g H4 H5) (subst0_weight_le v t1 t2 (S i) H2 (wadd f (S (weight_map f
 394 u2))) (wadd g (S (weight_map g u1))) (\lambda (m: nat).(wadd_le f g H4 (S
 395 (weight_map f u2)) (S (weight_map g u1)) (le_S (S (weight_map f u2))
 396 (weight_map g u1) (lt_le_S (weight_map f u2) (weight_map g u1) (H1 f g H4
 397 H5))) m)) (lt_le_S (weight_map (wadd f (S (weight_map f u2))) (lift (S (S i))
 398 O v)) (wadd g (S (weight_map g u1)) (S i)) (eq_ind nat (weight_map f (lift (S
 399 i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f (S
 400 (weight_map f u2))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f
 401 u2)) v (S i) f)))))))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_:
 402 (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall
 403 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
 404 (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt (weight_map f t2)
 405 (weight_map g t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
 406 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt
 407 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
 408 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O)
 409 t1)) (plus_lt_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
 410 O) t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O)
 411 (\lambda (m: nat).(le_S_n (wadd f O m) (wadd g O m) (le_n_S (wadd f O m)
 412 (wadd g O m) (wadd_le f g H4 O O (le_n O) m)))) (lt_le_S (weight_map (wadd f
 413 O) (lift (S (S i)) O v)) (wadd g O (S i)) (eq_ind nat (weight_map f (lift (S
 414 i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O) (lift (S
 415 (S i)) O v)) (lift_weight_add_O O v (S i) f)))))))))))))) (\lambda (t1:
 416 T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
 417 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
 418 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
 419 i))) \to (lt (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
 420 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
 421 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
 422 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
 423 (weight_map g u1) (weight_map (wadd g O) t1)) (plus_lt_compat (weight_map f
 424 u2) (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
 425 (H1 f g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(le_S_n (wadd f O
 426 m) (wadd g O m) (le_n_S (wadd f O m) (wadd g O m) (wadd_le f g H4 O O (le_n
 427 O) m)))) (lt_le_S (weight_map (wadd f O) (lift (S (S i)) O v)) (wadd g O (S
 428 i)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g
 429 i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v
 430 (S i) f)))))))))))))) b)) (\lambda (_: F).(\lambda (t1: T).(\lambda (t2:
 431 T).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H3: ((\forall (f0: ((nat \to
 432 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f0 m) (g m))))
 433 \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (lt (weight_map f0 t2)
 434 (weight_map g t1)))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
 435 \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
 436 (H5: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
 437 f0 u2) (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1))
 438 (plus_lt_compat (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2)
 439 (weight_map g t1) (H1 f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t
 440 z H))))).
 441
 442 theorem subst0_tlt_head:
 443  \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt
 444 (THead (Bind Abbr) u z) (THead (Bind Abbr) u t)))))
 445 \def
 446  \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
 447 z)).(lt_n_S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
 448 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z)) (plus
 449 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
 450 (weight_map (\lambda (_: nat).O) u))) t)) (plus_le_lt_compat (weight_map
 451 (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
 452 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z) (weight_map
 453 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (le_n
 454 (weight_map (\lambda (_: nat).O) u)) (subst0_weight_lt u t z O H (wadd
 455 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (wadd (\lambda
 456 (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (\lambda (m: nat).(le_n
 457 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u)) m)))
 458 (eq_ind nat (weight_map (\lambda (_: nat).O) (lift O O u)) (\lambda (n:
 459 nat).(lt n (S (weight_map (\lambda (_: nat).O) u)))) (eq_ind_r T u (\lambda
 460 (t0: T).(lt (weight_map (\lambda (_: nat).O) t0) (S (weight_map (\lambda (_:
 461 nat).O) u)))) (le_n (S (weight_map (\lambda (_: nat).O) u))) (lift O O u)
 462 (lift_r u O)) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda
 463 (_: nat).O) u))) (lift (S O) O u)) (lift_weight_add_O (S (weight_map (\lambda
 464 (_: nat).O) u)) u O (\lambda (_: nat).O))))))))).
 465
 466 theorem subst0_tlt:
 467  \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt z
 468 (THead (Bind Abbr) u t)))))
 469 \def
 470  \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
 471 z)).(tlt_trans (THead (Bind Abbr) u z) z (THead (Bind Abbr) u t) (tlt_head_dx
 472 (Bind Abbr) u z) (subst0_tlt_head u t z H))))).
 473