proposition: Lemma adde_EList1_new: ~ evalid g (u,v) -> Permutation ((u,v)::(EList g)) (EList EdgeListGG_adde).
proof: Proof. intros. unfold EdgeListGG_adde. simpl. unfold pregraph_add_edge. set (l:=(u,v)::EList g). unfold EList. destruct finiteE. simpl. destruct a. unfold addValidFunc in H1. simpl in H1. apply NoDup_Permutation. unfold l. apply NoDup_cons. rewrite EList_evalid. auto. apply NoDup_EList. auto. intros; split; intros. apply H1. destruct H2. right; auto. left. rewrite <- EList_evalid. apply H2. apply H1 in H2. unfold l. destruct H2. right. apply EList_evalid. auto. left. auto. 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