proposition: Lemma update_pri_by_key_not_In: forall h key newpri, ~In key (map heap_item_key h) -> update_pri_by_key h key newpri = h.
proof: Proof. induction h. reflexivity. intros. simpl. unfold update_pri_if_key. case Z.eq_dec; intro. exfalso. apply H. left. auto. rewrite IHh; trivial. intro. apply H. right. trivial. Qed.
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