DEFINITION weight_le()
TYPE =
       ∀t:T
         .∀f:nat→nat
           .∀g:nat→nat
             .∀n:nat.(le (f n) (g n))
               →le (weight_map f t) (weight_map g t)
BODY =
Show proof