DEFINITION weight_add_O()
TYPE =
       ∀t:T.(eq nat (weight_map (wadd λ:nat.O O) t) (weight_map λ:nat.O t))
BODY =
       assume t: T
          assume n: nat
             by (wadd_O .)
             we proved eq nat (wadd λ:nat.O O n) O
          we proved ∀n:nat.(eq nat (wadd λ:nat.O O n) O)
          by (weight_eq . . . previous)
          we proved eq nat (weight_map (wadd λ:nat.O O) t) (weight_map λ:nat.O t)
       we proved ∀t:T.(eq nat (weight_map (wadd λ:nat.O O) t) (weight_map λ:nat.O t))