fact: Definition rep2hi (r : reptype t_struct_edge) : heap_item := match r with (v1, (v2, v3)) => (force_int v1, (force_int v2, force_int v3)) end.
imports: VST.floyd.proofauto CertiGraph.floyd_ext.share CertiGraph.lib.List_ext CertiGraph.unionfind.env_unionfind_arr RelationClasses CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel Sorting CertiGraph.kruskal.spatial_wedgearray_graph CertiGraph.kruskal.kruskal_specs