DEFINITION lift_weight_add_O()
TYPE =
       ∀w:nat
         .∀t:T
           .∀h:nat
             .∀f:nat→nat
               .eq
                 nat
                 weight_map f (lift h O t)
                 weight_map (wadd f w) (lift (S h) O t)
BODY =
        assume w: nat
        assume t: T
        assume h: nat
        assume f: nat→nat
          (h1) 
              assume m: nat
              suppose H: lt m O
                by (lt_x_O . H .)
                we proved eq nat (wadd f w m) (f m)
∀m:nat.(lt m O)→(eq nat (wadd f w m) (f m))
          end of h1
          (h2) 
             by (plus_n_O .)
eq nat (wadd f w O) (plus (wadd f w O) O)
          end of h2
          (h3) 
              assume m: nat
              suppose : le O m
                by (refl_equal . .)
                we proved eq nat (f m) (f m)
                that is equivalent to eq nat (wadd f w (S m)) (f m)
∀m:nat.(le O m)→(eq nat (wadd f w (S m)) (f m))
          end of h3
          by (lift_weight_add . . . . . . h1 h2 h3)
          we proved 
             eq
               nat
               weight_map f (lift h O t)
               weight_map (wadd f w) (lift (S h) O t)
       we proved 
          ∀w:nat
            .∀t:T
              .∀h:nat
                .∀f:nat→nat
                  .eq
                    nat
                    weight_map f (lift h O t)
                    weight_map (wadd f w) (lift (S h) O t)