From 3a097260dac2ca73370a493b1f25975f3394f699 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Mon, 6 Aug 2018 13:40:50 -0400
Subject: Add related_iff_app_curried

---
 src/Util/Logic/ProdForall.v | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 src/Util/Logic/ProdForall.v

(limited to 'src/Util/Logic')

diff --git a/src/Util/Logic/ProdForall.v b/src/Util/Logic/ProdForall.v
new file mode 100644
index 000000000..f194b442b
--- /dev/null
+++ b/src/Util/Logic/ProdForall.v
@@ -0,0 +1,5 @@
+Require Export Crypto.Util.FixCoqMistakes.
+
+Lemma pull_prod_forall A A' B B' (Q : A * A' -> B * B' -> Prop)
+: (forall x y, Q x y) <-> (forall x0 y0 x1 y1, Q (x0, x1) (y0, y1)).
+Proof. intuition. Qed.
-- 
cgit v1.2.3