Add related_sigT_by_eq

1 files changed, 16 insertions, 0 deletions

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.