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