proposition: Theorem sort_sorted: forall (g:EdgeListGG) (l: list EType), sorted g (sort g l).
proof: Proof. induction l; intros. apply sorted_nil. destruct l. simpl. apply sorted_1. simpl in IHl. simpl. apply insert_sorted. 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