proposition: Lemma big_fset_incl (A : {fset I}) B F : A `<=` B -> (forall x, x \in B -> x \notin A -> F x = idx) -> \big[op/idx]_(x <- A) F x = \big[op/idx]_(x <- B) F x.
proof: Proof. move=> subAB Fid; rewrite [in RHS](big_fsetID (mem A)) /=. rewrite [X in op _ X]big1_fset ?Monoid.mulm1; last first. by move=> i; rewrite !inE /= => /andP[iB iNA _]; apply: Fid. by apply: eq_fbigl => i; rewrite !inE /= -(@in_fsetI _ B A) (fsetIidPr _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)