proposition: Lemma eremove_EList_rev: forall l, Permutation l (EList EdgeListGG_eremove) -> Permutation (e::l) (EList g).
proof: Proof. intros. assert (~ In e (EList EdgeListGG_eremove)). rewrite EList_evalid. apply eremove_evalid1. assert (~ In e l). unfold not; intros. apply (Permutation_in (l':= (EList EdgeListGG_eremove))) in H1. contradiction. auto. apply NoDup_Permutation. apply NoDup_cons; auto. apply NoDup_Perm_EList in H; auto. apply NoDup_EList. intros; split; intros. apply EList_evalid. destruct H2. subst x. auto. apply (Permutation_in (l':= (EList EdgeListGG_eremove))) in H2; auto. rewrite EList_evalid in H2. simpl in H2. unfold removeValidFunc in H2. apply H2. destruct (E_EqDec x e). unfold equiv in e0. subst x. left; auto. unfold complement, equiv in c. right. assert (evalid EdgeListGG_eremove x). apply remove_edge_evalid. split. apply EList_evalid in H2; auto. auto. rewrite <- EList_evalid in H3. apply (Permutation_in (l:= (EList EdgeListGG_eremove))). apply Permutation_sym; auto. apply H3. 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