proposition: Lemma lseg_eq (ls: listspec list_structid list_link list_token): forall dsh psh l v , is_pointer_or_null v -> lseg ls dsh psh l v v = !!(l=nil) && emp.
proof: Proof. intros. rewrite (lseg_unfold ls dsh psh l v v). destruct l. f_equal. f_equal. apply prop_ext; split; intro; auto. unfold ptr_eq. unfold is_pointer_or_null in H. destruct Archi.ptr64 eqn:Hp; destruct v; inv H; auto; unfold Ptrofs.cmpu; rewrite Ptrofs.eq_true; auto. destruct p. apply pred_ext; apply derives_extract_prop; intro. destruct H0. contradiction H1. destruct v; inv H; try split; auto; apply Ptrofs.eq_true. inv H0. 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