matita/matita/contribs/lambdadelta/basic_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 "Basic-1/subst0/defs.ma".
  18
  19 include "Basic-1/lift/props.ma".
  20
  21 include "Basic-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 (le_plus_plus (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)) (le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f O)
  65 t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O) (wadd
  66 g O) (\lambda (n: nat).(wadd_le f g H2 O O (le_n O) n))))))))) (\lambda (f:
  67 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
  68 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
  69 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)) (le_plus_plus (weight_map f u2)
  71 (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0) (H1 f
  72 g H2 H3) (weight_le t0 (wadd f O) (wadd g O) (\lambda (n: nat).(wadd_le f g
  73 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)) (le_plus_plus (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)) (le_plus_plus (weight_map f u0) (weight_map g u0) (weight_map (wadd f (S
 106 (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)) (le_plus_plus (weight_map f u0)
 122 (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)) (le_plus_plus (weight_map f u0) (weight_map g u0) (weight_map (wadd f O)
 136 t2) (weight_map (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O) (wadd g
 137 O) (\lambda (m: nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat (weight_map
 138 f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3 (weight_map (wadd f O)
 139 (lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f)))))))))))))))) b))
 140 (\lambda (_: F).(\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda
 141 (i: nat).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H1: ((\forall (f0: ((nat
 142 \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f0 m) (g
 143 m)))) \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (le (weight_map f0
 144 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to
 145 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0
 146 m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v)) (g
 147 i))).(le_n_S (plus (weight_map f0 u0) (weight_map f0 t2)) (plus (weight_map g
 148 u0) (weight_map g t1)) (le_plus_plus (weight_map f0 u0) (weight_map g u0)
 149 (weight_map f0 t2) (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2
 150 H3))))))))))))))) k)) (\lambda (v: T).(\lambda (u1: T).(\lambda (u2:
 151 T).(\lambda (i: nat).(\lambda (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall
 152 (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f
 153 m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le
 154 (weight_map f u2) (weight_map g u1)))))))).(\lambda (k: K).(K_ind (\lambda
 155 (k0: K).(\forall (t1: T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to
 156 (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
 157 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s
 158 k0 i))) \to (le (weight_map f t2) (weight_map g t1))))))) \to (\forall (f:
 159 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
 160 (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map
 161 f (THead k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b:
 162 B).(B_ind (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s
 163 (Bind b0) i) v t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat
 164 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f
 165 (lift (S (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (le (weight_map f
 166 t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g:
 167 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
 168 f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead (Bind b0) u2 t2))
 169 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda
 170 (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f:
 171 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
 172 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le
 173 (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to
 174 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f
 175 m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
 176 i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f
 177 u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
 178 t1)) (le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S
 179 (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1) (H1 f
 180 g H4 H5) (H3 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map g u1)))
 181 (\lambda (m: nat).(wadd_le f g H4 (S (weight_map f u2)) (S (weight_map g u1))
 182 (le_n_S (weight_map f u2) (weight_map g u1) (H1 f g H4 H5)) m)) (eq_ind nat
 183 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5
 184 (weight_map (wadd f (S (weight_map f u2))) (lift (S (S i)) O v))
 185 (lift_weight_add_O (S (weight_map f u2)) v (S i) f))))))))))))) (\lambda (t1:
 186 T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
 187 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
 188 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
 189 i))) \to (le (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
 190 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
 191 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
 192 i))).(le_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
 193 (weight_map g u1) (weight_map (wadd g O) t1)) (le_plus_plus (weight_map f u2)
 194 (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1) (H1 f
 195 g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f g H4 O O
 196 (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n:
 197 nat).(lt n (g i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v))
 198 (lift_weight_add_O O v (S i) f))))))))))))) (\lambda (t1: T).(\lambda (t2:
 199 T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to
 200 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
 201 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le (weight_map f
 202 t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
 203 \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5:
 204 (lt (weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u2)
 205 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O)
 206 t1)) (le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f O)
 207 t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O)
 208 (\lambda (m: nat).(wadd_le f g H4 O O (le_n O) m)) (eq_ind nat (weight_map f
 209 (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O)
 210 (lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) b))
 211 (\lambda (_: F).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 i v t1
 212 t2)).(\lambda (H3: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
 213 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
 214 (S i) O v)) (g i)) \to (le (weight_map f0 t2) (weight_map g
 215 t1)))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to
 216 nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda (H5:
 217 (lt (weight_map f0 (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f0 u2)
 218 (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1)) (le_plus_plus
 219 (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2) (weight_map g t1) (H1
 220 f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t z H))))).
 221 (* COMMENTS
 222 Initial nodes: 4101
 223 END *)
 224
 225 theorem subst0_weight_lt:
 226  \forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
 227 u t z) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 228 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 229 d) O u)) (g d)) \to (lt (weight_map f z) (weight_map g t))))))))))
 230 \def
 231  \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (d: nat).(\lambda
 232 (H: (subst0 d u t z)).(subst0_ind (\lambda (n: nat).(\lambda (t0: T).(\lambda
 233 (t1: T).(\lambda (t2: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 234 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 235 n) O t0)) (g n)) \to (lt (weight_map f t2) (weight_map g t1))))))))))
 236 (\lambda (v: T).(\lambda (i: nat).(\lambda (f: ((nat \to nat))).(\lambda (g:
 237 ((nat \to nat))).(\lambda (_: ((\forall (m: nat).(le (f m) (g m))))).(\lambda
 238 (H1: (lt (weight_map f (lift (S i) O v)) (g i))).H1)))))) (\lambda (v:
 239 T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i: nat).(\lambda (_: (subst0 i
 240 v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 241 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 242 i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map g u1)))))))).(\lambda
 243 (t0: T).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (f: ((nat \to
 244 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
 245 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
 246 k0 u2 t0)) (weight_map g (THead k0 u1 t0)))))))) (\lambda (b: B).(B_ind
 247 (\lambda (b0: B).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 248 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 249 i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t0)) (weight_map g
 250 (THead (Bind b0) u1 t0)))))))) (\lambda (f: ((nat \to nat))).(\lambda (g:
 251 ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g
 252 m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S
 253 (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f u2))) t0)) (plus
 254 (weight_map g u1) (weight_map (wadd g (S (weight_map g u1))) t0))
 255 (lt_le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S
 256 (weight_map f u2))) t0) (weight_map (wadd g (S (weight_map g u1))) t0) (H1 f
 257 g H2 H3) (weight_le t0 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map
 258 g u1))) (\lambda (n: nat).(wadd_lt f g H2 (S (weight_map f u2)) (S
 259 (weight_map g u1)) (lt_n_S (weight_map f u2) (weight_map g u1) (H1 f g H2
 260 H3)) n))))))))) (\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
 261 nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt
 262 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
 263 (weight_map (wadd f O) t0)) (plus (weight_map g u1) (weight_map (wadd g O)
 264 t0)) (lt_le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f
 265 O) t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O)
 266 (wadd g O) (\lambda (n: nat).(le_S_n (wadd f O n) (wadd g O n) (le_n_S (wadd
 267 f O n) (wadd g O n) (wadd_le f g H2 O O (le_n O) n))))))))))) (\lambda (f:
 268 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
 269 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
 270 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t0)) (plus
 271 (weight_map g u1) (weight_map (wadd g O) t0)) (lt_le_plus_plus (weight_map f
 272 u2) (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
 273 (H1 f g H2 H3) (weight_le t0 (wadd f O) (wadd g O) (\lambda (n: nat).(le_S_n
 274 (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
 275 O (le_n O) n))))))))))) b)) (\lambda (_: F).(\lambda (f0: ((nat \to
 276 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0
 277 m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v)) (g
 278 i))).(lt_n_S (plus (weight_map f0 u2) (weight_map f0 t0)) (plus (weight_map g
 279 u1) (weight_map g t0)) (lt_le_plus_plus (weight_map f0 u2) (weight_map g u1)
 280 (weight_map f0 t0) (weight_map g t0) (H1 f0 g H2 H3) (weight_le t0 f0 g
 281 H2)))))))) k))))))))) (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (v:
 282 T).(\forall (t2: T).(\forall (t1: T).(\forall (i: nat).((subst0 (s k0 i) v t1
 283 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 284 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 285 (s k0 i)) O v)) (g (s k0 i))) \to (lt (weight_map f t2) (weight_map g
 286 t1))))))) \to (\forall (u0: T).(\forall (f: ((nat \to nat))).(\forall (g:
 287 ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map
 288 f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead k0 u0 t2))
 289 (weight_map g (THead k0 u0 t1))))))))))))))) (\lambda (b: B).(B_ind (\lambda
 290 (b0: B).(\forall (v: T).(\forall (t2: T).(\forall (t1: T).(\forall (i:
 291 nat).((subst0 (s (Bind b0) 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 (Bind b0) i)) O v)) (g (s (Bind b0) i)))
 294 \to (lt (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0:
 295 T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
 296 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to
 297 (lt (weight_map f (THead (Bind b0) u0 t2)) (weight_map g (THead (Bind b0) u0
 298 t1))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda
 299 (i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\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 i)) O v)) (g (S i))) \to (lt
 302 (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f:
 303 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m:
 304 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
 305 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f (S (weight_map f
 306 u0))) t2)) (plus (weight_map g u0) (weight_map (wadd g (S (weight_map g u0)))
 307 t1)) (le_lt_plus_plus (weight_map f u0) (weight_map g u0) (weight_map (wadd f
 308 (S (weight_map f u0))) t2) (weight_map (wadd g (S (weight_map g u0))) t1)
 309 (weight_le u0 f g H2) (H1 (wadd f (S (weight_map f u0))) (wadd g (S
 310 (weight_map g u0))) (\lambda (m: nat).(wadd_le f g H2 (S (weight_map f u0))
 311 (S (weight_map g u0)) (le_n_S (weight_map f u0) (weight_map g u0) (weight_le
 312 u0 f g H2)) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n:
 313 nat).(lt n (g i))) H3 (weight_map (wadd f (S (weight_map f u0))) (lift (S (S
 314 i)) O v)) (lift_weight_add_O (S (weight_map f u0)) v (S i) f))))))))))))))))
 315 (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda
 316 (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to
 317 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
 318 \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt (weight_map f
 319 t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to
 320 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f
 321 m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g
 322 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f O) t2)) (plus
 323 (weight_map g u0) (weight_map (wadd g O) t1)) (le_lt_plus_plus (weight_map f
 324 u0) (weight_map g u0) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
 325 (weight_le u0 f g H2) (H1 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f
 326 g H2 O O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda
 327 (n: nat).(lt n (g i))) H3 (weight_map (wadd f O) (lift (S (S i)) O v))
 328 (lift_weight_add_O O v (S i) f)))))))))))))))) (\lambda (v: T).(\lambda (t2:
 329 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1
 330 t2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 331 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 332 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
 333 t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat
 334 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3:
 335 (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u0)
 336 (weight_map (wadd f O) t2)) (plus (weight_map g u0) (weight_map (wadd g O)
 337 t1)) (le_lt_plus_plus (weight_map f u0) (weight_map g u0) (weight_map (wadd f
 338 O) t2) (weight_map (wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O) (wadd
 339 g O) (\lambda (m: nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat
 340 (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3
 341 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v (S i)
 342 f)))))))))))))))) b)) (\lambda (_: F).(\lambda (v: T).(\lambda (t2:
 343 T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 i v t1
 344 t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
 345 nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
 346 (S i) O v)) (g i)) \to (lt (weight_map f0 t2) (weight_map g
 347 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
 348 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
 349 (H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
 350 f0 u0) (weight_map f0 t2)) (plus (weight_map g u0) (weight_map g t1))
 351 (le_lt_plus_plus (weight_map f0 u0) (weight_map g u0) (weight_map f0 t2)
 352 (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2 H3))))))))))))))) k))
 353 (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda
 354 (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall
 355 (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
 356 (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f u2) (weight_map
 357 g u1)))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t1:
 358 T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to
 359 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
 360 \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (lt
 361 (weight_map f t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to
 362 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
 363 \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead
 364 k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b: B).(B_ind
 365 (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s (Bind b0) i) v
 366 t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 367 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 368 (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (lt (weight_map f t2)
 369 (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat
 370 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f
 371 (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead (Bind b0) u2 t2))
 372 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda
 373 (t2: T).(\lambda (H2: (subst0 (S i) v t1 t2)).(\lambda (_: ((\forall (f:
 374 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
 375 (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt
 376 (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to
 377 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f
 378 m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
 379 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f (S (weight_map f
 380 u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
 381 t1)) (lt_le_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f
 382 (S (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1) (H1
 383 f g H4 H5) (subst0_weight_le v t1 t2 (S i) H2 (wadd f (S (weight_map f u2)))
 384 (wadd g (S (weight_map g u1))) (\lambda (m: nat).(wadd_lt f g H4 (S
 385 (weight_map f u2)) (S (weight_map g u1)) (lt_n_S (weight_map f u2)
 386 (weight_map g u1) (H1 f g H4 H5)) m)) (eq_ind nat (weight_map f (lift (S i) O
 387 v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f (S (weight_map f
 388 u2))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f u2)) v (S i)
 389 f))))))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v
 390 t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 391 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
 392 (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g
 393 t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
 394 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt
 395 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2)
 396 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O)
 397 t1)) (lt_plus_plus (weight_map f u2) (weight_map g u1) (weight_map (wadd f O)
 398 t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O)
 399 (\lambda (m: nat).(le_S_n (wadd f O m) (wadd g O m) (le_n_S (wadd f O m)
 400 (wadd g O m) (wadd_le f g H4 O O (le_n O) m)))) (eq_ind nat (weight_map f
 401 (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O)
 402 (lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) (\lambda
 403 (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3:
 404 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
 405 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S
 406 i))) \to (lt (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat
 407 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le
 408 (f m) (g m))))).(\lambda (H5: (lt (weight_map f (lift (S i) O v)) (g
 409 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
 410 (weight_map g u1) (weight_map (wadd g O) t1)) (lt_plus_plus (weight_map f u2)
 411 (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1) (H1 f
 412 g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(le_S_n (wadd f O m)
 413 (wadd g O m) (le_n_S (wadd f O m) (wadd g O m) (wadd_le f g H4 O O (le_n O)
 414 m)))) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g
 415 i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v
 416 (S i) f))))))))))))) b)) (\lambda (_: F).(\lambda (t1: T).(\lambda (t2:
 417 T).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H3: ((\forall (f0: ((nat \to
 418 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f0 m) (g m))))
 419 \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (lt (weight_map f0 t2)
 420 (weight_map g t1)))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
 421 \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
 422 (H5: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map
 423 f0 u2) (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1))
 424 (lt_plus_plus (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2)
 425 (weight_map g t1) (H1 f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t
 426 z H))))).
 427 (* COMMENTS
 428 Initial nodes: 4207
 429 END *)
 430
 431 theorem subst0_tlt_head:
 432  \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt
 433 (THead (Bind Abbr) u z) (THead (Bind Abbr) u t)))))
 434 \def
 435  \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
 436 z)).(lt_n_S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
 437 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z)) (plus
 438 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
 439 (weight_map (\lambda (_: nat).O) u))) t)) (le_lt_plus_plus (weight_map
 440 (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
 441 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) z) (weight_map
 442 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (le_n
 443 (weight_map (\lambda (_: nat).O) u)) (subst0_weight_lt u t z O H (wadd
 444 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (wadd (\lambda
 445 (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) (\lambda (m: nat).(le_n
 446 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u)) m)))
 447 (eq_ind nat (weight_map (\lambda (_: nat).O) (lift O O u)) (\lambda (n:
 448 nat).(lt n (S (weight_map (\lambda (_: nat).O) u)))) (eq_ind_r T u (\lambda
 449 (t0: T).(lt (weight_map (\lambda (_: nat).O) t0) (S (weight_map (\lambda (_:
 450 nat).O) u)))) (le_n (S (weight_map (\lambda (_: nat).O) u))) (lift O O u)
 451 (lift_r u O)) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda
 452 (_: nat).O) u))) (lift (S O) O u)) (lift_weight_add_O (S (weight_map (\lambda
 453 (_: nat).O) u)) u O (\lambda (_: nat).O))))))))).
 454 (* COMMENTS
 455 Initial nodes: 347
 456 END *)
 457
 458 theorem subst0_tlt:
 459  \forall (u: T).(\forall (t: T).(\forall (z: T).((subst0 O u t z) \to (tlt z
 460 (THead (Bind Abbr) u t)))))
 461 \def
 462  \lambda (u: T).(\lambda (t: T).(\lambda (z: T).(\lambda (H: (subst0 O u t
 463 z)).(tlt_trans (THead (Bind Abbr) u z) z (THead (Bind Abbr) u t) (tlt_head_dx
 464 (Bind Abbr) u z) (subst0_tlt_head u t z H))))).
 465 (* COMMENTS
 466 Initial nodes: 59
 467 END *)
 468