proposition: Lemma linked_correctly_app3: forall contents contents' lookup, linked_correctly contents lookup -> linked_correctly' contents' lookup (Zlength contents) -> linked_correctly (contents ++ contents') lookup.
proof: Proof. repeat intro. destruct H as [Hz H]. destruct H0 as [Hz' H0]. split. trivial. intros. rewrite Z.add_0_l. assert (0 <= i < Zlength contents \/ Zlength contents <= i < Zlength (contents ++ contents')) by rep_lia. destruct H2. destruct H2. unfold loc. rewrite Znth_app1; try lia. apply H; trivial. rep_lia. unfold loc. rewrite Znth_app2; try lia. rewrite Zlength_app in *. specialize (H0 (i - Zlength contents)). destruct H0. lia. rewrite H3. 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