!v:nat.(eq nat -> nat -> nat \x:nat.\y:nat.(plus y v) \x:nat.\y:nat.O)

Fare cut di:
 (eq nat -> nat \w:nat.(plus w v) \w:nat.(plus (plus w w) v))
e poi riscriverlo