proposition: Lemma edgeless_GG_EList: EList edgeless_GG = nil.
proof: Proof. unfold edgeless_GG, EList. destruct finiteE. simpl in *. destruct a. destruct x; [trivial | exfalso]. assert (In e (e::x)) by (apply in_eq). apply (H0 e). 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