proposition: Lemma sedge_equiv_in (G : sgraph) (A : {set G}) : {in A & &, equivalence_rel (connect (restrict A (--)))}.
proof: Proof. exact: in3W (sedge_in_equiv A). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)