fact: Definition heap_item_rep (i : heap_item) : wedgerep := (Vint (fst i), (Vint (fst (snd i)), Vint (snd (snd i)))).
imports: VST.floyd.proofauto Coq.ZArith.ZArith CertiGraph.floyd_ext.closed_lemmas CertiGraph.kruskal.kruskal_edgelist RelationClasses CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel