proposition: Lemma sep_sep X p q : [fset x in sep X p | q x] = [fset x in X | p x && q x].
proof: Proof. apply: fset_ext => x. by rewrite !in_sep andbA. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)