proposition: Lemma lseg_neq (ls: listspec list_structid list_link list_token): forall dsh psh s v v2, ptr_neq v v2 -> lseg ls dsh psh s v v2 = lseg_cons ls dsh psh s v v2.
proof: Proof. intros. rewrite lseg_unroll. apply pred_ext. apply orp_left; auto. rewrite andp_assoc. do 2 (apply derives_extract_prop; intro). congruence. apply orp_right2. 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