proposition: Lemma linked_correctly_app_eq: forall contents contents' lookup, (linked_correctly contents lookup /\ linked_correctly' contents' lookup (Zlength contents)) = linked_correctly (contents ++ contents') lookup.
proof: Proof. intros. apply prop_ext. split; intros. eapply linked_correctly_app3; tauto. split. eapply linked_correctly_app1; apply H. apply linked_correctly_app2. 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