proposition: Lemma eq_diso (T : finType) (e1 e2 : rel T) (e1_sym : symmetric e1) (e1_irrefl : irreflexive e1) (e2_sym : symmetric e2) (e2_irrefl : irreflexive e2) : e1 =2 e2 -> diso (SGraph e1_sym e1_irrefl) (SGraph e2_sym e2_irrefl).
proof: Proof. intro E. exists (@bij_id T); abstract (move => x y /=; by rewrite /edge_rel /= E). Defined.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)