proposition: Lemma eremove_EList: forall l, Permutation (e::l) (EList g) -> Permutation l (EList UAdjMatGG_eremove).
proof: Proof. intros. assert (Hel: NoDup (e::l)). apply NoDup_Perm_EList in H; auto. apply NoDup_Permutation. apply NoDup_cons_1 in Hel; auto. apply NoDup_EList. intros. rewrite EList_evalid. simpl. unfold removeValidFunc. rewrite <- EList_evalid. split; intros. split. apply (Permutation_in (l:=(e::l))). apply H. right; auto. unfold not; intros. subst e. apply NoDup_cons_2 in Hel. contradiction. destruct H0. apply Permutation_sym in H. apply (Permutation_in (l':=(e::l))) in H0. 2: auto. destruct H0. symmetry in H0; contradiction. auto. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.find_lemmas CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.undirected_graph CertiGraph.graph.MathAdjMatGraph