proposition: Lemma uf_union_sym: forall g1 g2 e1 e2, uf_union g1 e1 e2 g2 -> uf_union g1 e2 e1 g2.
proof: Proof. intros. repeat intro. specialize (H S2 S1 H1 H0 H3 H2). assert (Same_set (Union Vertex S1 S2) (Union Vertex S2 S1)). { rewrite Same_set_spec. hnf. intros. split; intro; destruct H4; [right | left | right | left]; auto. } destruct H as [? [? ?]]. split; [|split]. - destruct H; [left; rewrite H4; auto | right]. destruct H as [rt [? ?]]. pose proof (app_same_set H4). exists rt. split; [rewrite H8 | intros; rewrite H8]; auto. - intros. apply H5; auto. - intros. specialize (H6 _ H7). destruct H6; [left; rewrite H4 | right]; auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.Ensembles_ext CertiGraph.lib.EnumEnsembles CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable