From e294cfbd559677f6ffe219d96158373e886f3615 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 16 Nov 2018 22:06:53 -0500
Subject: Add related_sigT_by_eq

---
 src/Util/Sigma/Related.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 src/Util/Sigma/Related.v

(limited to 'src/Util')

diff --git a/src/Util/Sigma/Related.v b/src/Util/Sigma/Related.v
new file mode 100644
index 000000000..ac98f7629
--- /dev/null
+++ b/src/Util/Sigma/Related.v
@@ -0,0 +1,16 @@
+Import EqNotations.
+
+Definition related_sigT_by_eq {A P1 P2} (R : forall x : A, P1 x -> P2 x -> Prop)
+           (x : @sigT A P1) (y : @sigT A P2)
+  : Prop
+  := { pf : projT1 x = projT1 y
+     | R _ (rew pf in projT2 x) (projT2 y) }.
+
+Definition map_related_sigT_by_eq {A P1 P2} {R1 R2 : forall x : A, P1 x -> P2 x -> Prop}
+           (HR : forall x v1 v2, R1 x v1 v2 -> R2 x v1 v2)
+           (x : @sigT A P1) (y : @sigT A P2)
+  : @related_sigT_by_eq A P1 P2 R1 x y -> @related_sigT_by_eq A P1 P2 R2 x y.
+Proof using Type.
+  destruct x, y; cbv [related_sigT_by_eq projT1 projT2].
+  intro H; exists (proj1_sig H); apply HR, (proj2_sig H).
+Qed.
-- 
cgit v1.2.3