proposition: Lemma linked_correctly_app2: forall contents contents' lookup, linked_correctly (contents ++ contents') lookup -> linked_correctly' contents' lookup (Zlength contents).
proof: Proof. repeat intro. destruct H as [Hz H]. split; trivial. intros. specialize (H (Zlength contents + i)). rewrite Znth_app2 in H. 2: lia. rewrite Z.add_0_l in H. replace (Zlength contents + i - Zlength contents) with i in H by lia. apply H. 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