proposition: Lemma update_pri_by_key_keys_unaffected: forall l key newpri, map heap_item_key (update_pri_by_key l key newpri) = map heap_item_key l.
proof: Proof. intros. induction l; trivial. simpl. rewrite IHl. f_equal. unfold update_pri_by_key, update_pri_if_key, heap_item_key. destruct (Z.eq_dec key (fst (fst a))); simpl fst; 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