proposition: Lemma fimsetU1 (aT rT : choiceType) (f : aT -> rT) (B : {fset aT}) a : [fset f x | x <- a |` B] = f a |` [fset f x | x <- B].
proof: Proof. by rewrite fimsetU fimset1. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)