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