proposition: Lemma allU X Y p : all p (X `|` Y) = all p X && all p Y.
proof: Proof. rewrite -all_cat. apply/idP/idP; apply: sub_all_dom => ?; by rewrite mem_cat !inE. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)