proposition: Lemma sub_val_eq (T : eqType) (P : pred T) (u : [the subType P of {x : T | P x}]) x (Px : x \in P) : (u == Sub x Px) = (val u == x).
proof: Proof. by case: (SubP u) => {u} u Pu. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)