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