proposition: Lemma heap_array_split: forall L1 L2 ptr, heap_array (L1 ++ L2) ptr = ((heap_array L1 ptr) * (heap_array L2 (field_address0 (tarray t_item (Zlength (L1 ++ L2))) [ArraySubsc (Zlength L1)] ptr)))%logic.
proof: Proof. intros. unfold heap_array. rewrite map_app. erewrite split2_data_at_Tarray_app. 2: rewrite Zlength_map; reflexivity. 2: rewrite Zlength_app, Zlength_map; lia. rewrite Zlength_app. replace (Zlength L1 + Zlength L2 - Zlength L1) with (Zlength L2) by lia. 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