proposition: Lemma big_undup (I : eqType) (r : seq I) (P : pred I) F : idempotent op -> \big[op/x]_(i <- undup r | P i) F i = \big[op/x]_(i <- r | P i) F i.
proof: Proof. move=> opxx; rewrite -!(big_filter _ _ _ P) filter_undup. elim: {P r}(filter P r) => //= i r IHr. case: ifP => [r_i | _]; rewrite !big_cons {}IHr //. by rewrite (big_rem_AC _ _ r_i) opA /= opxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)