proposition: Lemma reindex (I J : finType) (h : J -> I) (P : pred I) (F : I -> X) : {on [pred i | P i], bijective h} -> \big[*%M/1]_(i | P i) F i ≡ \big[*%M/1]_(j | P (h j)) F (h j).
proof: Proof. case=> h' hK h'K; rewrite (reindex_onto h h' h'K). by apply eqv_bigl => j; rewrite !inE; case Pi: (P _); rewrite //= hK ?eqxx. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect)