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