proposition: Lemma eq_imfset (f f' : K -> V) (p q : finmempred _): f =1 f' -> (forall x, in_mem x p = in_mem x q) -> imfset key f p = imfset key f' q.
proof: Proof. move=> eq_f eqP; apply/fsetP => x; apply/imfsetP/imfsetP => /= [] [k Pk ->]; by exists k => //=; rewrite ?eq_f ?eqP in Pk *. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)