Some theorems about objdesign-of-var and the functions to read and write variables.
Theorem:
(defthm objdesign-of-var-aux-iff-read-auto-var-aux (iff (objdesign-of-var-aux var frame scopes) (read-auto-var-aux var scopes)))
Theorem:
(defthm objdesign-of-var-when-valuep-of-read-var (implies (valuep (read-var id compst)) (objdesign-of-var id compst)))
Theorem:
(defthm write-auto-var-aux-iff-objdesign-of-var-aux (iff (write-auto-var-aux var val scopes) (objdesign-of-var-aux var frame scopes)))
Theorem:
(defthm objdesignp-of-objdesign-of-var-when-valuep-of-read-var (implies (valuep (read-var id compst)) (objdesignp (objdesign-of-var id compst))))