DEFINITION lift_weight_map()
TYPE =
       ∀t:T
         .∀h:nat
           .∀d:nat
             .∀f:nat→nat
               .∀m:nat.(le d m)→(eq nat (f m) O)
                 →eq nat (weight_map f (lift h d t)) (weight_map f t)
BODY =
Show proof