proposition: Lemma lookup_oob_eq_trans: forall contents lookup lookup' lookup'', lookup_oob_eq contents lookup lookup' -> lookup_oob_eq contents lookup' lookup'' -> lookup_oob_eq contents lookup lookup''.
proof: Proof. intros. destruct H, H0. split. transitivity lookup'; auto. repeat intro. specialize (H1 i H3). rewrite H1. apply H2; 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