proposition: Lemma tagged_eq (T : eqType) (T_ : T -> eqType) (x : T) (u v : T_ x) : (⟨ x , u ⟩ == ⟨ x , v ⟩) = (u == v).
proof: Proof. by rewrite -tag_eqE/tag_eq/= eqxx tagged_asE. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)