From 063c874f4bd87911cff3466542d599b579f2ff2d Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Mon, 29 Oct 2018 16:45:10 -0400
Subject: Add some lemmas about ex, and, eq

---
 _CoqProject                  |  1 +
 src/Util/Logic/ExistsEqAnd.v | 26 ++++++++++++++++++++++++++
 2 files changed, 27 insertions(+)
 create mode 100644 src/Util/Logic/ExistsEqAnd.v

diff --git a/_CoqProject b/_CoqProject
index 54f1cd4f7..659c23407 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6546,6 +6546,7 @@ src/Util/ListUtil/FoldBool.v
 src/Util/ListUtil/Forall.v
 src/Util/ListUtil/ForallIn.v
 src/Util/ListUtil/SetoidList.v
+src/Util/Logic/ExistsEqAnd.v
 src/Util/Logic/ImplAnd.v
 src/Util/Logic/ProdForall.v
 src/Util/MSetPositive/Equality.v
diff --git a/src/Util/Logic/ExistsEqAnd.v b/src/Util/Logic/ExistsEqAnd.v
new file mode 100644
index 000000000..27f08eb89
--- /dev/null
+++ b/src/Util/Logic/ExistsEqAnd.v
@@ -0,0 +1,26 @@
+Require Import Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Tactics.DestructHead.
+
+Local Ltac t :=
+  repeat first [ progress destruct_head'_ex
+               | progress destruct_head'_and
+               | progress intros
+               | progress subst
+               | assumption
+               | progress repeat esplit ].
+
+Lemma ex_and_eq_l_iff {A P x}
+  : (exists y : A, y = x /\ P y) <-> P x.
+Proof. t. Qed.
+
+Lemma ex_and_eq_r_iff {A P x}
+  : (exists y : A, x = y /\ P y) <-> P x.
+Proof. t. Qed.
+
+Lemma ex_eq_and_l_iff {A P x}
+  : (exists y : A, P y /\ y = x) <-> P x.
+Proof. t. Qed.
+
+Lemma ex_eq_and_r_iff {A P x}
+  : (exists y : A, P y /\ x = y) <-> P x.
+Proof. t. Qed.
-- 
cgit v1.2.3