proposition: Lemma lookup_oob_eq_nil: forall L1 L2, lookup_oob_eq nil L1 L2 -> L1 = L2.
proof: Proof. intros. destruct H. apply Znth_eq_ext. apply Permutation_Zlength; trivial. intros. apply H0. intros. rewrite Zlength_nil in H2. 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