Theorems about w.
Theorem: plist-worldp-of-w-when-state-p
(defthm plist-worldp-of-w-when-state-p (implies (state-p state) (plist-worldp (w state))))
