proposition: Lemma find_item_by_key_app: forall L1 L2 k, find_item_by_key (L1 ++ L2) k = find_item_by_key L1 k ++ find_item_by_key L2 k.
proof: Proof. intros. unfold find_item_by_key. rewrite filter_app. 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