proposition: Lemma sepU X Y p : [fset x in X `|` Y | p x] = [fset x in X | p x] `|` [fset x in Y | p x].
proof: Proof. apply: fset_ext => x. rewrite !inE. by bcase. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)