proposition: Lemma linked_correctly'_app: forall L1 L1' L2 n, linked_correctly' (L1 ++ L1') L2 n <-> (linked_correctly' L1 L2 n /\ linked_correctly' L1' L2 (Zlength L1 + n)).
proof: Proof. split; intros. destruct H. split; split; trivial; repeat intro. subst loc. assert (0 <= i < Zlength (L1 ++ L1')) by (rewrite Zlength_app; rep_lia). specialize (H0 _ H2). destruct H0. rewrite app_Znth1 in *; try lia. subst loc. assert (0 <= i + Zlength L1 < Zlength (L1 ++ L1')) by (rewrite Zlength_app; rep_lia). specialize (H0 _ H2). destruct H0. rewrite app_Znth2 in *; try lia. replace (i + Zlength L1 - Zlength L1) with i in * by lia. replace (Zlength L1 + n + i) with (n + (i + Zlength L1)) by lia. auto. destruct H as [[? ?] [? ?]]. split; trivial. intros. subst loc. rewrite Zlength_app in H3. assert (0 <= i < Zlength L1 \/ 0 <= i - Zlength L1 < Zlength L1') by rep_lia. destruct H4. rewrite app_Znth1; auto; lia. rewrite app_Znth2; try lia. specialize (H2 _ H4). destruct H2. replace (Zlength L1 + n + (i - Zlength L1)) with (n + i) in H5 by lia. auto. 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