proposition: Lemma closure_pred2 e x y : connect_sym e -> closure e (pred2 x y) =i [predU closure e (pred1 x) & closure e (pred1 y)].
proof: Proof. move => sym_e z; rewrite !inE /= -!closure1 // !inE. apply/closureP/idP => [[? /pred2P [->|->]]|/orP[]]; rewrite sym_e; try by move->. by exists x; rewrite // !inE eqxx. by exists y; rewrite // !inE eqxx. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)