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