proposition: Lemma find_item_by_key_update_pri_by_key': forall L k1 k2 np, k1 <> k2 -> find_item_by_key (update_pri_by_key L k1 np) k2 = find_item_by_key L k2.
proof: Proof. intros. unfold find_item_by_key, update_pri_by_key. rewrite filter_absorb_map. trivial. intros. unfold update_pri_if_key, heap_item_key. destruct x as [[? ?] ?]. simpl. case Z.eq_dec; intro; simpl. subst k1. split; trivial. case Z.eq_dec; auto; intro; simpl. contradiction. case Z.eq_dec; simpl; split; auto. 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