proposition: Lemma lseg_cons_eq (ls: listspec list_structid list_link list_token): forall sh h r x z , lseg ls sh (h::r) x z = !!(~ ptr_eq x z) && (EX y : val, !!(is_pointer_or_null y) && list_token sh x * list_cell ls sh h x * field_at sh list_struct (StructField list_link :: nil) (valinject (nested_field_type list_struct (StructField list_link :: nil)) y) x * lseg ls sh r y z).
proof: Proof. intros. rewrite lseg_unroll. apply pred_ext. apply orp_left. rewrite andp_assoc. apply derives_extract_prop; intro. apply derives_extract_prop; intro. inv H0. unfold lseg_cons. normalize. symmetry in H0; inv H0. apply exp_right with y. normalize. apply orp_right2. unfold lseg_cons. apply andp_derives; auto. apply exp_right with h. apply exp_right with r. apply exp_derives; intro y. normalize. autorewrite with subst norm1 norm2; 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