proposition: Lemma big_uniq : forall (I : finType) (r : seq I) F, uniq r -> \big[*%M/1]_(i <- r) F i === \big[*%M/1]_(i | i \in r) F i.
proof: Proof. move=> I r F uniq_r; rewrite <- (big_filter (index_enum I)); apply: eq_big_perm. by rewrite filter_index_enum uniq_perm_eq ?enum_uniq // => i; rewrite mem_enum. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops