proposition: Lemma imfset_inv (aT : finType) (rT : choiceType) (f : aT -> rT) (y : [fset f x | x in aT]) : Σ x : aT, f x = val y.
proof: Proof. suff E : exists x, f x == val y by exists (xchoose E); rewrite (eqP (xchooseP E)). case/imfsetP : (valP y) => /= x _ ->. by exists x. Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries)