proposition: Lemma pimsetP (aT rT : finType) (f : aT -> option rT) (A : {set aT}) x : reflect (exists2 x0, x0 \in A & f x0 == Some x) (x \in pimset f A).
proof: Proof. rewrite inE. exact: (iffP exists_inP). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)