proposition: Lemma Permutation_find_item_by_key: forall L1 L2 k, Permutation L1 L2 -> Permutation (find_item_by_key L1 k) (find_item_by_key L2 k).
proof: Proof. intros. unfold find_item_by_key. apply Permutation_filter. 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