proposition: Theorem sort_perm: forall (g: EdgeListGG) l, Permutation l (sort g l).
proof: Proof. induction l. simpl. apply Permutation_refl. simpl. apply (Permutation_trans (l':=a::(sort g l))). apply perm_skip. apply IHl. apply insert_perm. 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