proposition: Lemma eqv_bigr (I : Type) (r : seq I) (P : pred I) (F1 F2 : I -> X) : (forall i : I, P i -> F1 i ≡ F2 i) -> \big[*%M/1]_(i <- r | P i) F1 i ≡ \big[*%M/1]_(i <- r | P i) F2 i.
proof: Proof. elim/big_rec2 : _ => // i x y Pi H1 H2. by rewrite H2 ?H1. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)