proposition: Lemma linked_correctly_app1: forall contents contents' lookup, linked_correctly (contents ++ contents') lookup -> linked_correctly contents lookup.
proof: Proof. repeat intro. destruct H. split; trivial. repeat intro. specialize (H0 i). rewrite Znth_app1 in H0. 2: lia. apply H0. rewrite Zlength_app. 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