proposition: Lemma eq_fclosure (f f' : T -> T) a : f =1 f' -> fclosure f a =i fclosure f' a.
proof: Proof. move => eq_f; apply: eq_closure. exact: eq_fconnect. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)