proposition: Lemma imset_pre_val (T : finType) (P : pred T) (s : subFinType P) (A : {set T}) : A \subset P -> val @: (val @^-1: A : {set s}) = A.
proof: Proof. move=> /subsetP A_P. apply/setP=> x; apply/imsetP/idP. + case=> y; by rewrite inE => ? ->. + move=> x_A; by exists (Sub x (A_P x x_A)); rewrite ?inE SubK. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)