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 =
Show proof