proposition: Lemma lookup_oob_eq_refl: forall contents lookup, lookup_oob_eq contents lookup lookup.
proof: Proof. split. trivial. repeat intro. 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