proposition: Lemma lseg_cons_eq2: forall (ls : listspec list_structid list_link list_token) (dsh psh : share) (h : elemtype ls) (r : list (val * elemtype ls)) (x x' z : val), lseg ls dsh psh ((x',h) :: r) x z = !!(x=x' /\ ~ ptr_eq x z) && (EX y : val, lseg_cell ls dsh psh h x y * lseg ls dsh psh r y z).
proof: Proof. intros. rewrite -> lseg_cons_eq. unfold lseg_cell. 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