proposition: Lemma data_at_singleton_array_eq': forall (sh : Share.t) (t : type) (v : reptype t) (p : val), data_at sh (Tarray t 1 noattr) [v] p = data_at sh t v p.
proof: Proof. intros. apply data_at_singleton_array_eq. auto. Qed.
imports: VST.floyd.proofauto VST.floyd.library CertiGraph.floyd_ext.share CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.graph_relation CertiGraph.msl_application.ArrayGraph CertiGraph.unionfind.env_unionfind_arr CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.kruskal.spatial_wedgearray_graph CertiGraph.kruskal.kruskal_specs CertiGraph.graph.undirected_uf_lemmas