proposition: Lemma eq_closure e e' a : connect e =2 connect e' -> closure e a =i closure e' a.
proof: Proof. by move => eq_e z; apply/closureP/closureP => -[x ?]; exists x => //; rewrite ?eq_e // -eq_e. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)