proposition: Lemma eremove_uforest': uforest' g -> uforest' EdgeListGG_eremove /\ ~ connected EdgeListGG_eremove (src g e) (dst g e).
proof: Proof. intros. destruct e as (u,v) eqn:X. rewrite src_fst, dst_snd; auto. pose proof eremove_evalid1. assert (Hvvalid: forall v1 : VType, vvalid EdgeListGG_eremove v1 <-> vvalid g v1). simpl; intros; split; auto. split. { split. intros. simpl. apply H. apply H1. split. intros. unfold adj_edge, strong_evalid in H1; simpl in H1. unfold removeValidFunc in H1. destruct H1. destruct H1. destruct H2. destruct H. destruct H5. apply (H5 u0 v0). split; split. split. apply H1. apply H1. apply H3. split. apply H2. apply H2. apply H4. split. intros. apply evalid_strong_evalid; auto. unfold unique_simple_upath; intros. assert (exists l, fits_upath EdgeListGG_eremove l p1). apply valid_upath_exists_list_edges. apply H2. destruct H5 as [l1 ?]. assert (exists l, fits_upath EdgeListGG_eremove l p2). apply valid_upath_exists_list_edges. apply H4. destruct H6 as [l2 ?]. destruct (in_dec E_EqDec e l1). apply (fits_upath_evalid EdgeListGG_eremove p1) in i; auto. contradiction. destruct (in_dec E_EqDec e l2). apply (fits_upath_evalid EdgeListGG_eremove p2) in i; auto. contradiction. apply (fits_upath_transfer' p1 l1 _ g) in H5; auto. apply (fits_upath_transfer' p2 l2 _ g) in H6; auto. assert (valid_upath g p1). apply valid_upath_exists_list_edges'. exists l1. auto. assert (valid_upath g p2). apply valid_upath_exists_list_edges'. exists l2. auto. assert (unique_simple_upath g). apply H. unfold unique_simple_upath in H9. destruct H1. destruct H3. destruct H2. destruct H4. apply (H9 u0 v0 p1 p2). split; auto. split; auto. split; auto. split; auto. intros. apply (fits_upath_evalid _ _ _ _ H6) in H7. apply H7. intros. apply (fits_upath_evalid _ _ _ _ H5) in H7. apply H7. } { unfold not, connected; intros. destruct H1 as [p ?]. assert (exists l, fits_upath EdgeListGG_eremove l p). apply valid_upath_exists_list_edges. apply H1. destruct H2 as [l ?]. assert (fits_upath g l p). apply (sound_fits_upath_transfer p l EdgeListGG_eremove g); auto. intros. apply (fits_upath_evalid _ _ _ _ H2) in H3. apply H3. assert (connected_by_path g p u v). split. apply valid_upath_exists_list_edges'. exists l; auto. destruct H1. auto. pose proof (forest_bridge1 g u v H e_evalid). assert (In (u,v) l). unfold bridge in H5. apply (H5 p l); auto. apply (fits_upath_evalid _ _ _ _ H2) in H6. rewrite X in *. contradiction. } Qed.
imports: VST.floyd.proofauto CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph CertiGraph.graph.undirected_graph