proposition: Lemma edgeless_graph_EList: EList edgeless_graph = nil.
proof: Proof. intros. unfold edgeless_graph, 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.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