DEFINITION weight_add_O()
TYPE =
       ∀t:T.(eq nat (weight_map (wadd λ:nat.O O) t) (weight_map λ:nat.O t))
BODY =
Show proof