# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1231075139 18000
# Node ID 71ade09024ac59331d6d3afce9202c820a46468a
# Parent  8caa3b3f8fc0aec71794563467599e95a4ab66cb
Quibbly note on [eq] in first-order logic

diff -r 8caa3b3f8fc0 -r 71ade09024ac src/Predicates.v
--- 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 *)