proposition: Lemma eqv_big_bij (I1 I2 : finType) (f : I1 -> I2) (r1 : seq I1) (r2 : seq I2) (P1 : pred I1) (P2 : pred I2) (F1 : I1 -> X) (F2 : I2 -> X) : perm_eq r2 (map f r1) -> (forall x, P1 x = P2 (f x)) -> (forall i : I1, P1 i -> F1 i ≡ F2 (f i)) -> \big[*%M/1]_(i <- r1 | P1 i) F1 i ≡ \big[*%M/1]_(i <- r2 | P2 i) F2 i.
proof: Proof. move => pr HP HF. rewrite (perm_big _ _ pr). exact: eqv_map. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)