proposition: Lemma cons_eq: forall {A: Type} (l l': list A) (a: A), l = l' -> a::l = a::l'.
proof: Proof. intros. rewrite H. auto. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.graph.FiniteGraph CertiGraph.kruskal.env_kruskal_edgelist