proposition: Lemma evalid_uv_vvalid: forall (g: EdgeListGG) u v, evalid g (u,v) -> vvalid g u /\ vvalid g v.
proof: Proof. intros. apply evalid_strong_evalid in H. destruct H. destruct H0. rewrite src_fst in H0 by auto. rewrite dst_snd in H1 by auto. split. apply H0. apply H1. 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