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