proposition: Lemma lseg_nonnull (ls: listspec list_structid list_link list_token): forall dsh psh s v, typed_true (tptr list_struct) v -> lseg ls dsh psh s v nullval = lseg_cons ls dsh psh s v nullval.
proof: Proof. intros. unfold nullval. apply lseg_neq. destruct v; inv H; intuition; try congruence. intro. apply ptr_eq_e in H. destruct Archi.ptr64 eqn:Hp; inv H. inv H1. intro. simpl in H. destruct Archi.ptr64; congruence. 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