proposition: Lemma fimsetU (aT rT : choiceType) (f : aT -> rT) (A B : {fset aT}) : [fset f x | x <- A `|` B] = [fset f x | x <- A] `|` [fset f x | x <- B].
proof: Proof. apply/eqP. rewrite eqEsub fsubUset !fimsetS ?fsubUl ?fsubUr ?andbT //. apply/subP => x /fimsetP [a] /fsetUP [H|H] ->; by rewrite inE (in_fimset _ H). Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)