DEFINITION lift_weight()
TYPE =
       ∀t:T.∀h:nat.∀d:nat.(eq nat (weight (lift h d t)) (weight t))
BODY =
        assume t: T
        assume h: nat
        assume d: nat
           assume m: nat
           suppose : le d m
             by (refl_equal . .)
             we proved eq nat O O
          we proved ∀m:nat.(le d m)→(eq nat O O)
          by (lift_weight_map . . . . previous)
          we proved eq nat (weight_map λ:nat.O (lift h d t)) (weight_map λ:nat.O t)
          that is equivalent to eq nat (weight (lift h d t)) (weight t)
       we proved ∀t:T.∀h:nat.∀d:nat.(eq nat (weight (lift h d t)) (weight t))