Quibbly note on [eq] in first-order logic
author Adam Chlipala Sun, 04 Jan 2009 08:18:59 -0500 8caa3b3f8fc0 cbf2f74a5130 src/Predicates.v 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
```--- a/src/Predicates.v	Sat Jan 03 19:57:02 2009 -0500
+++ b/src/Predicates.v	Sun Jan 04 08:18:59 2009 -0500
@@ -354,7 +354,7 @@
ex_intro : forall x : A, P x -> ex P
]] *)

-(** [ex] is parameterized by the type [A] that we quantify over, and by a predicate [P] over [A]s.  We prove an existential by exhibiting some [x] of type [A], along with a proof of [P x].  As usual, there are tactics that save us from worrying about the low-level details most of the time. *)
+(** [ex] is parameterized by the type [A] that we quantify over, and by a predicate [P] over [A]s.  We prove an existential by exhibiting some [x] of type [A], along with a proof of [P x].  As usual, there are tactics that save us from worrying about the low-level details most of the time.  We use the equality operator [=], which, depending on the settings in which they learned logic, different people will say either is or is not part of first-order logic.  For our purposes, it is. *)

Theorem exist1 : exists x : nat, x + 1 = 2.
(* begin thide *)```