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