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 =
        assume t: T
        assume f: nat→nat
        assume g: nat→nat
        suppose H: ∀n:nat.(eq nat (f n) (g n))
          (h1) 
             assume n: nat
                (h1) 
                   by (le_n .)
le (g n) (g n)
                end of h1
                (h2) 
                   by (H .)
eq nat (f n) (g n)
                end of h2
                by (eq_ind_r . . . h1 . h2)
                we proved le (f n) (g n)
             we proved ∀n:nat.(le (f n) (g n))
             by (weight_le . . . previous)
le (weight_map f t) (weight_map g t)
          end of h1
          (h2) 
             assume n: nat
                (h1) 
                   by (le_n .)
le (g n) (g n)
                end of h1
                (h2) 
                   by (H .)
eq nat (f n) (g n)
                end of h2
                by (eq_ind_r . . . h1 . h2)
                we proved le (g n) (f n)
             we proved ∀n:nat.(le (g n) (f n))
             by (weight_le . . . previous)
le (weight_map g t) (weight_map f t)
          end of h2
          by (le_antisym . . h1 h2)
          we proved eq nat (weight_map f t) (weight_map g t)
       we proved 
          ∀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)