proposition: Lemma lseg_cons_right_list (ls: listspec list_structid list_link list_token): forall sh l l' x h y z, sepalg.nonidentity sh -> list_token sh y * list_cell ls sh h y * field_at sh list_struct (StructField list_link :: nil) (valinject (nested_field_type list_struct (StructField list_link :: nil)) z) y * lseg ls sh l x y * lseg ls sh l' z nullval |-- lseg ls sh (l++h::nil) x z * lseg ls sh l' z nullval.
proof: Proof. intros. destruct l'. rewrite lseg_nil_eq. pose proof ptr_eq_nullval. normalize. apply lseg_cons_right_null. rewrite lseg_cons_eq. Intros u. Exists u. rewrite !prop_true_andp by auto. rewrite <- !sepcon_assoc. apply sepcon_derives; auto. pull_right (list_cell ls sh e z). pull_right (list_token sh z). apply sepcon_derives; auto. apply sepcon_derives; auto. apply lseg_cons_right_neq. auto. 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