proposition: Lemma big_sep (T R : choiceType) (idx : R) (op : Monoid.com_law idx) (F : T -> R) (X : {fset T}) p: \big[op/idx]_(i <- [fset x in X | p x]) F i = \big[op/idx]_(i <- X | p i) F i.
proof: Proof. rewrite -(big_filter _ p). apply: perm_big. apply: uniq_perm; try by rewrite ?filter_uniq // funiq. move => x. by rewrite !inE mem_filter andbC. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)