fact: Definition keys_dist_linked_correctly i keys dist h := forall k, Znth i keys = k -> find_item_by_key (heap_items h) k = [(k, Znth i dist, Int.repr i)] \/ ~ In k (proj_keys h).
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel