example : Prop := ∃ y : Nat, ∀ x : Nat, y = x