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