proposition: Lemma sep_sub X X' p q : X `<=` X' -> {in X, subpred p q} -> [fset x in X | p x] `<=` [fset x in X' | q x].
proof: Proof. move => /subP subX sub_p. apply/subP => x. rewrite !inE => /andP [? ?]. rewrite subX //=. exact: sub_p. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)