blob: ac98f76297099306712067d03a7b20188c6f6b30 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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.
|
