proposition: Lemma lseg_cons_right_neq (ls: listspec list_structid list_link list_token): forall sh l x h y w 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 * field_at sh list_struct (StructField list_link :: nil) (valinject (nested_field_type list_struct (StructField list_link :: nil)) w) z |-- lseg ls sh (l++h::nil) x z * field_at sh list_struct (StructField list_link :: nil) (valinject (nested_field_type list_struct (StructField list_link :: nil)) w) z.
proof: Proof. intros. unfold lseg. normalize. apply exp_right with (al ++ (y,h)::nil). rewrite prop_true_andp by (rewrite map_app; reflexivity). eapply derives_trans; [ | apply LsegGeneral.lseg_cons_right_neq; auto]. cancel. 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