DEFINITION plus_O()
TYPE =
       ∀x:nat
         .∀y:nat.(eq nat (plus x y) O)→(land (eq nat x O) (eq nat y O))
BODY =
Show proof