proposition: Lemma fsetUSU X X' Y Y' : X `<=` X' -> Y `<=` Y' -> X `|` Y `<=` X' `|` Y'.
proof: Proof. move => H1 H2. by rewrite fsubUset (sub_trans H1 _) ?(sub_trans H2 _) // ?fsubUl ?fsubUr. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)