How objdesign-of-var changes under enter-scope.
Theorem: objdesign-of-var-of-enter-scope
(defthm objdesign-of-var-of-enter-scope (equal (objdesign-of-var var (enter-scope compst)) (objdesign-of-var var compst)))
