proposition: Lemma fimsetP X (f : T -> T') a : reflect (exists2 x, x \in X & a = f x) (a \in f `@` X).
proof: Proof. rewrite fimsetE set_ofE. exact: mapP. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)