Equivalence of write-object and write-var for object designators of variables.
Theorem:
(defthm write-object-of-objdesign-of-var-to-write-var (b* ((objdes (objdesign-of-var var compst))) (implies objdes (equal (write-object objdes val compst) (write-var var val compst)))))