proposition: Lemma eq_closed (e e' : rel T) (a : {pred T}) : e =2 e' -> closed e a <-> closed e' a.
proof: Proof. rewrite /closed_mem => eq_e. by split => cl x y; [rewrite -eq_e|rewrite eq_e]; apply: cl. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)