proposition: Lemma unfold_lseg_cons (ls: listspec list_structid list_link list_token): forall P Q1 Q R e dsh psh s, PROPx P (LOCALx (Q1::Q) (SEPx (lseg ls dsh psh s e nullval :: R))) |-- !! (typed_true (tptr list_struct) e) -> PROPx P (LOCALx (Q1::Q) (SEPx (lseg ls dsh psh s e nullval :: R))) |-- EX hryp: elemtype ls * list (val * elemtype ls) * val * val, match hryp with (h,r,y,p) => !! (s=(p,h)::r /\ is_pointer_or_null y) && !! (p=e)&& PROPx P (LOCALx Q (SEPx (list_token dsh e :: list_cell ls dsh h e :: field_at psh list_struct (StructField list_link :: nil) (valinject (nested_field_type list_struct (StructField list_link :: nil)) y) e :: lseg ls dsh psh r y nullval :: R))) end.
proof: Proof. intros. apply unfold_lseg_neq. eapply derives_trans. apply H. normalize. unfold local. super_unfold_lift. unfold nullval. intro. apply ptr_eq_e in H1. subst. normalize. Qed.
imports: VST.floyd.base2 VST.floyd.client_lemmas VST.floyd.closed_lemmas VST.floyd.nested_pred_lemmas VST.floyd.nested_field_lemmas VST.floyd.efield_lemmas VST.floyd.mapsto_memory_block VST.floyd.reptype_lemmas VST.floyd.data_at_rec_lemmas VST.floyd.field_at VST.floyd.nested_loadstore VST.floyd.entailer