proposition: Lemma valK' (T : Type) (P : pred T) (sT : subType P) (x : sT) (p : P (val x)) : Sub (val x) p = x.
proof: Proof. apply: val_inj. by rewrite SubK. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)