proposition: Lemma imset_valT (T : finType) (P : pred T) (s : subFinType P) : val @: [set: s] = finset P.
proof: Proof. apply/setP=> z; apply/imsetP/idP; rewrite inE. + case=> y _ ->; exact: (valP y). + move=> z_P; by exists (Sub z z_P); last rewrite SubK. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)