proposition: Lemma g2wedgelist_evalid: forall g w, In w (graph_to_wedgelist g) -> evalid g (snd w).
proof: Proof. intros. apply list_in_map_inv in H. destruct H; destruct H. apply EList_evalid in H0. unfold edge_to_wedge in H. inversion H. simpl. 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