proposition: Lemma fimsetS X Y (f : T -> T') : X `<=` Y -> f `@` X `<=` f `@` Y.
proof: Proof. move/subP => S. apply/subP => y /fimsetP [x /S inX ->]. exact: in_fimset. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)