proposition: Lemma val_subset (T: finType) (H : {set T}) (A B : {set sig [eta mem H]}) : (val @: A \subset val @: B) = (A \subset B).
proof: Proof. by rewrite inj_imsetS //; exact: val_inj. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)