DEFINITION weight_add_S()
TYPE =
       ∀t:T
         .∀m:nat
           .le
             weight_map (wadd λ:nat.O O) t
             weight_map (wadd λ:nat.O (S m)) t
BODY =
Show proof