proposition: Lemma lookup_oob_eq_shuffle: forall contents contents' lookup lookup', Permutation (map heap_item_key contents) (map heap_item_key contents') -> lookup_oob_eq contents lookup lookup' -> lookup_oob_eq contents' lookup lookup'.
proof: Proof. repeat intro. destruct H0 as [Hz H0]. split; trivial. intros. apply H0. repeat intro. symmetry in H. apply Permutation_Znth in H. 2: exact 0. destruct H as [? [f [? [? ?]]]]. do 2 rewrite Zlength_map in *. rewrite <- H in *. apply (H1 (Z.of_nat (f (Z.to_nat j)))). specialize (H4 (Z.to_nat j)). rep_lia. specialize (H6 j H2). rewrite Znth_map in H6. 2: lia. rewrite H6 in H3. rewrite Znth_map in H3. trivial. specialize (H4 (Z.to_nat j)). rep_lia. 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