proposition: Lemma Sub_map (T : eqType) (P : {pred T}) (s : subType P) {A : seq (sub_type s)} (x : T) (Px : P x) : (Sub x Px \in A) = (x \in map val A).
proof: Proof. by rewrite -[X in X \in map val _](SubK s Px) mem_map. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)