matita/matita/contribs/lambdadelta/basic_1/tlt/props.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "Basic-1/tlt/defs.ma".
  18
  19 theorem wadd_le:
  20  \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n:
  21 nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((le v w) \to
  22 (\forall (n: nat).(le (wadd f v n) (wadd g w n))))))))
  23 \def
  24  \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H:
  25 ((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w:
  26 nat).(\lambda (H0: (le v w)).(\lambda (n: nat).(nat_ind (\lambda (n0:
  27 nat).(le (wadd f v n0) (wadd g w n0))) H0 (\lambda (n0: nat).(\lambda (_: (le
  28 (wadd f v n0) (wadd g w n0))).(H n0))) n))))))).
  29 (* COMMENTS
  30 Initial nodes: 81
  31 END *)
  32
  33 theorem wadd_lt:
  34  \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n:
  35 nat).(le (f n) (g n)))) \to (\forall (v: nat).(\forall (w: nat).((lt v w) \to
  36 (\forall (n: nat).(le (wadd f v n) (wadd g w n))))))))
  37 \def
  38  \lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H:
  39 ((\forall (n: nat).(le (f n) (g n))))).(\lambda (v: nat).(\lambda (w:
  40 nat).(\lambda (H0: (lt v w)).(\lambda (n: nat).(nat_ind (\lambda (n0:
  41 nat).(le (wadd f v n0) (wadd g w n0))) (le_S_n v w (le_S (S v) w H0))
  42 (\lambda (n0: nat).(\lambda (_: (le (wadd f v n0) (wadd g w n0))).(H n0)))
  43 n))))))).
  44 (* COMMENTS
  45 Initial nodes: 95
  46 END *)
  47
  48 theorem wadd_O:
  49  \forall (n: nat).(eq nat (wadd (\lambda (_: nat).O) O n) O)
  50 \def
  51  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (wadd (\lambda (_:
  52 nat).O) O n0) O)) (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat
  53 (wadd (\lambda (_: nat).O) O n0) O)).(refl_equal nat O))) n).
  54 (* COMMENTS
  55 Initial nodes: 53
  56 END *)
  57
  58 theorem weight_le:
  59  \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
  60 nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t)
  61 (weight_map g t)))))
  62 \def
  63  \lambda (t: T).(T_ind (\lambda (t0: T).(\forall (f: ((nat \to
  64 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
  65 \to (le (weight_map f t0) (weight_map g t0)))))) (\lambda (n: nat).(\lambda
  66 (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (_: ((\forall
  67 (n0: nat).(le (f n0) (g n0))))).(le_n (weight_map g (TSort n))))))) (\lambda
  68 (n: nat).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda
  69 (H: ((\forall (n0: nat).(le (f n0) (g n0))))).(H n))))) (\lambda (k:
  70 K).(K_ind (\lambda (k0: K).(\forall (t0: T).(((\forall (f: ((nat \to
  71 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
  72 \to (le (weight_map f t0) (weight_map g t0)))))) \to (\forall (t1:
  73 T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
  74 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g t1))))))
  75 \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
  76 (n: nat).(le (f n) (g n)))) \to (le (weight_map f (THead k0 t0 t1))
  77 (weight_map g (THead k0 t0 t1))))))))))) (\lambda (b: B).(B_ind (\lambda (b0:
  78 B).(\forall (t0: T).(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
  79 nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f t0)
  80 (weight_map g t0)))))) \to (\forall (t1: T).(((\forall (f: ((nat \to
  81 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
  82 \to (le (weight_map f t1) (weight_map g t1)))))) \to (\forall (f: ((nat \to
  83 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
  84 \to (le (match b0 with [Abbr \Rightarrow (S (plus (weight_map f t0)
  85 (weight_map (wadd f (S (weight_map f t0))) t1))) | Abst \Rightarrow (S (plus
  86 (weight_map f t0) (weight_map (wadd f O) t1))) | Void \Rightarrow (S (plus
  87 (weight_map f t0) (weight_map (wadd f O) t1)))]) (match b0 with [Abbr
  88 \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g (S (weight_map g
  89 t0))) t1))) | Abst \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g
  90 O) t1))) | Void \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g O)
  91 t1)))])))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to
  92 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
  93 \to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
  94 (H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
  95 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g
  96 t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
  97 nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus
  98 (weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1)) (plus
  99 (weight_map g t0) (weight_map (wadd g (S (weight_map g t0))) t1))
 100 (le_plus_plus (weight_map f t0) (weight_map g t0) (weight_map (wadd f (S
 101 (weight_map f t0))) t1) (weight_map (wadd g (S (weight_map g t0))) t1) (H f g
 102 H1) (H0 (wadd f (S (weight_map f t0))) (wadd g (S (weight_map g t0)))
 103 (\lambda (n: nat).(wadd_le f g H1 (S (weight_map f t0)) (S (weight_map g t0))
 104 (le_n_S (weight_map f t0) (weight_map g t0) (H f g H1)) n))))))))))))
 105 (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to nat))).(\forall (g:
 106 ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (weight_map f
 107 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f:
 108 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n)
 109 (g n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat
 110 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le
 111 (f n) (g n))))).(le_n_S (plus (weight_map f t0) (weight_map (wadd f O) t1))
 112 (plus (weight_map g t0) (weight_map (wadd g O) t1)) (le_plus_plus (weight_map
 113 f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map (wadd g O) t1)
 114 (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O
 115 (le_n O) n)))))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to
 116 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
 117 \to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
 118 (H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
 119 (n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g
 120 t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
 121 nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus
 122 (weight_map f t0) (weight_map (wadd f O) t1)) (plus (weight_map g t0)
 123 (weight_map (wadd g O) t1)) (le_plus_plus (weight_map f t0) (weight_map g t0)
 124 (weight_map (wadd f O) t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f
 125 O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O (le_n O) n))))))))))))
 126 b)) (\lambda (_: F).(\lambda (t0: T).(\lambda (H: ((\forall (f0: ((nat \to
 127 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f0 n) (g n))))
 128 \to (le (weight_map f0 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
 129 (H0: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
 130 (n: nat).(le (f0 n) (g n)))) \to (le (weight_map f0 t1) (weight_map g
 131 t1))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to
 132 nat))).(\lambda (H1: ((\forall (n: nat).(le (f0 n) (g n))))).(le_n_S (plus
 133 (weight_map f0 t0) (weight_map f0 t1)) (plus (weight_map g t0) (weight_map g
 134 t1)) (le_plus_plus (weight_map f0 t0) (weight_map g t0) (weight_map f0 t1)
 135 (weight_map g t1) (H f0 g H1) (H0 f0 g H1))))))))))) k)) t).
 136 (* COMMENTS
 137 Initial nodes: 1309
 138 END *)
 139
 140 theorem weight_eq:
 141  \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
 142 nat))).(((\forall (n: nat).(eq nat (f n) (g n)))) \to (eq nat (weight_map f
 143 t) (weight_map g t)))))
 144 \def
 145  \lambda (t: T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
 146 nat))).(\lambda (H: ((\forall (n: nat).(eq nat (f n) (g n))))).(le_antisym
 147 (weight_map f t) (weight_map g t) (weight_le t f g (\lambda (n:
 148 nat).(eq_ind_r nat (g n) (\lambda (n0: nat).(le n0 (g n))) (le_n (g n)) (f n)
 149 (H n)))) (weight_le t g f (\lambda (n: nat).(eq_ind_r nat (g n) (\lambda (n0:
 150 nat).(le (g n) n0)) (le_n (g n)) (f n) (H n)))))))).
 151 (* COMMENTS
 152 Initial nodes: 121
 153 END *)
 154
 155 theorem weight_add_O:
 156  \forall (t: T).(eq nat (weight_map (wadd (\lambda (_: nat).O) O) t)
 157 (weight_map (\lambda (_: nat).O) t))
 158 \def
 159  \lambda (t: T).(weight_eq t (wadd (\lambda (_: nat).O) O) (\lambda (_:
 160 nat).O) (\lambda (n: nat).(wadd_O n))).
 161 (* COMMENTS
 162 Initial nodes: 23
 163 END *)
 164
 165 theorem weight_add_S:
 166  \forall (t: T).(\forall (m: nat).(le (weight_map (wadd (\lambda (_: nat).O)
 167 O) t) (weight_map (wadd (\lambda (_: nat).O) (S m)) t)))
 168 \def
 169  \lambda (t: T).(\lambda (m: nat).(weight_le t (wadd (\lambda (_: nat).O) O)
 170 (wadd (\lambda (_: nat).O) (S m)) (\lambda (n: nat).(wadd_le (\lambda (_:
 171 nat).O) (\lambda (_: nat).O) (\lambda (_: nat).(le_n O)) O (S m) (le_S O m
 172 (le_O_n m)) n)))).
 173 (* COMMENTS
 174 Initial nodes: 61
 175 END *)
 176
 177 theorem tlt_trans:
 178  \forall (v: T).(\forall (u: T).(\forall (t: T).((tlt u v) \to ((tlt v t) \to
 179 (tlt u t)))))
 180 \def
 181  \lambda (v: T).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (lt (weight u)
 182 (weight v))).(\lambda (H0: (lt (weight v) (weight t))).(lt_trans (weight u)
 183 (weight v) (weight t) H H0))))).
 184 (* COMMENTS
 185 Initial nodes: 43
 186 END *)
 187
 188 theorem tlt_head_sx:
 189  \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt u (THead k u t))))
 190 \def
 191  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
 192 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) (THead
 193 k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
 194 (t: T).(lt (weight_map (\lambda (_: nat).O) u) (match b0 with [Abbr
 195 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
 196 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
 197 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
 198 (\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
 199 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
 200 (u: T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) u) (plus
 201 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
 202 (weight_map (\lambda (_: nat).O) u))) t)) (le_plus_l (weight_map (\lambda (_:
 203 nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_:
 204 nat).O) u))) t))))) (\lambda (u: T).(\lambda (t: T).(le_n_S (weight_map
 205 (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u) (weight_map
 206 (wadd (\lambda (_: nat).O) O) t)) (le_plus_l (weight_map (\lambda (_: nat).O)
 207 u) (weight_map (wadd (\lambda (_: nat).O) O) t))))) (\lambda (u: T).(\lambda
 208 (t: T).(le_n_S (weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda
 209 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)) (le_plus_l
 210 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O)
 211 t))))) b)) (\lambda (_: F).(\lambda (u: T).(\lambda (t: T).(le_n_S
 212 (weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u)
 213 (weight_map (\lambda (_: nat).O) t)) (le_plus_l (weight_map (\lambda (_:
 214 nat).O) u) (weight_map (\lambda (_: nat).O) t)))))) k).
 215 (* COMMENTS
 216 Initial nodes: 379
 217 END *)
 218
 219 theorem tlt_head_dx:
 220  \forall (k: K).(\forall (u: T).(\forall (t: T).(tlt t (THead k u t))))
 221 \def
 222  \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (u: T).(\forall (t: T).(lt
 223 (weight_map (\lambda (_: nat).O) t) (weight_map (\lambda (_: nat).O) (THead
 224 k0 u t)))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (u: T).(\forall
 225 (t: T).(lt (weight_map (\lambda (_: nat).O) t) (match b0 with [Abbr
 226 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
 227 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) | Abst
 228 \Rightarrow (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (wadd
 229 (\lambda (_: nat).O) O) t))) | Void \Rightarrow (S (plus (weight_map (\lambda
 230 (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) O) t)))]))))) (\lambda
 231 (u: T).(\lambda (t: T).(lt_le_trans (weight_map (\lambda (_: nat).O) t) (S
 232 (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda (_:
 233 nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_:
 234 nat).O) u))) t))) (lt_n_Sn (weight_map (\lambda (_: nat).O) t)) (le_n_S
 235 (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
 236 (weight_map (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O)
 237 u))) t)) (le_trans (weight_map (\lambda (_: nat).O) t) (weight_map (wadd
 238 (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t) (plus
 239 (weight_map (\lambda (_: nat).O) u) (weight_map (wadd (\lambda (_: nat).O) (S
 240 (weight_map (\lambda (_: nat).O) u))) t)) (eq_ind nat (weight_map (wadd
 241 (\lambda (_: nat).O) O) t) (\lambda (n: nat).(le n (weight_map (wadd (\lambda
 242 (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t))) (weight_add_S t
 243 (weight_map (\lambda (_: nat).O) u)) (weight_map (\lambda (_: nat).O) t)
 244 (weight_add_O t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
 245 (wadd (\lambda (_: nat).O) (S (weight_map (\lambda (_: nat).O) u))) t)))))))
 246 (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map (\lambda (_:
 247 nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus
 248 (weight_map (\lambda (_: nat).O) u) n)))) (le_n_S (weight_map (\lambda (_:
 249 nat).O) t) (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
 250 nat).O) t)) (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map
 251 (\lambda (_: nat).O) t))) (weight_map (wadd (\lambda (_: nat).O) O) t)
 252 (weight_add_O t)))) (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map
 253 (\lambda (_: nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_:
 254 nat).O) t) (S (plus (weight_map (\lambda (_: nat).O) u) n)))) (le_n_S
 255 (weight_map (\lambda (_: nat).O) t) (plus (weight_map (\lambda (_: nat).O) u)
 256 (weight_map (\lambda (_: nat).O) t)) (le_plus_r (weight_map (\lambda (_:
 257 nat).O) u) (weight_map (\lambda (_: nat).O) t))) (weight_map (wadd (\lambda
 258 (_: nat).O) O) t) (weight_add_O t)))) b)) (\lambda (_: F).(\lambda (u:
 259 T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) t) (plus
 260 (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))
 261 (le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
 262 nat).O) t)))))) k).
 263 (* COMMENTS
 264 Initial nodes: 659
 265 END *)
 266
 267 theorem tlt_wf__q_ind:
 268  \forall (P: ((T \to Prop))).(((\forall (n: nat).((\lambda (P0: ((T \to
 269 Prop))).(\lambda (n0: nat).(\forall (t: T).((eq nat (weight t) n0) \to (P0
 270 t))))) P n))) \to (\forall (t: T).(P t)))
 271 \def
 272  let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t:
 273 T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to
 274 Prop))).(\lambda (H: ((\forall (n: nat).(\forall (t: T).((eq nat (weight t)
 275 n) \to (P t)))))).(\lambda (t: T).(H (weight t) t (refl_equal nat (weight
 276 t)))))).
 277 (* COMMENTS
 278 Initial nodes: 61
 279 END *)
 280
 281 theorem tlt_wf_ind:
 282  \forall (P: ((T \to Prop))).(((\forall (t: T).(((\forall (v: T).((tlt v t)
 283 \to (P v)))) \to (P t)))) \to (\forall (t: T).(P t)))
 284 \def
 285  let Q \def (\lambda (P: ((T \to Prop))).(\lambda (n: nat).(\forall (t:
 286 T).((eq nat (weight t) n) \to (P t))))) in (\lambda (P: ((T \to
 287 Prop))).(\lambda (H: ((\forall (t: T).(((\forall (v: T).((lt (weight v)
 288 (weight t)) \to (P v)))) \to (P t))))).(\lambda (t: T).(tlt_wf__q_ind
 289 (\lambda (t0: T).(P t0)) (\lambda (n: nat).(lt_wf_ind n (Q (\lambda (t0:
 290 T).(P t0))) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0)
 291 \to (Q (\lambda (t0: T).(P t0)) m))))).(\lambda (t0: T).(\lambda (H1: (eq nat
 292 (weight t0) n0)).(let H2 \def (eq_ind_r nat n0 (\lambda (n1: nat).(\forall
 293 (m: nat).((lt m n1) \to (\forall (t1: T).((eq nat (weight t1) m) \to (P
 294 t1)))))) H0 (weight t0) H1) in (H t0 (\lambda (v: T).(\lambda (H3: (lt
 295 (weight v) (weight t0))).(H2 (weight v) H3 v (refl_equal nat (weight
 296 v))))))))))))) t)))).
 297 (* COMMENTS
 298 Initial nodes: 179
 299 END *)
 300