proposition: Lemma tm_eqv_equivalence: Equivalence tm_eqv.
proof: Proof. constructor. now intro. intros ?? H X f. specialize (H X f). by symmetry. intros ??? H H' X f. specialize (H X f). specialize (H' X f). etransitivity. apply H. apply H'. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures pttdom)