proposition: Lemma lseg_nonnull (ls: listspec list_structid list_link list_token): forall sh s v, typed_true (tptr list_struct) v -> lseg ls sh s v nullval = lseg_cons ls sh s v nullval.
proof: Proof. intros. unfold nullval. apply lseg_neq. unfold typed_true, strict_bool_val in H. simpl in H. destruct Archi.ptr64 eqn:Hp. * destruct v; inv H. destruct (Int64.eq i Int64.zero); inv H1. intro; apply ptr_eq_e in H; inv H. * destruct v; inv H. destruct (Int.eq i Int.zero); inv H1. intro; apply ptr_eq_e in H; inv H. 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