DEFINITION lift_weight_add()
TYPE =
       ∀w:nat
         .∀t:T
           .∀h:nat
             .∀d:nat
               .∀f:nat→nat
                 .∀g:nat→nat
                   .∀m:nat.(lt m d)→(eq nat (g m) (f m))
                     →(eq nat (g d) w
                          →(∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
                               →(eq
                                    nat
                                    weight_map f (lift h d t)
                                    weight_map g (lift (S h) d t))))
BODY =
Show proof