Converse of read-object-of-objdesign-of-var-to-read-var.
Theorem: read-var-to-read-object-of-objdesign-of-var
(defthm read-var-to-read-object-of-objdesign-of-var (b* ((objdes (objdesign-of-var var compst))) (implies objdes (equal (read-var var compst) (read-object objdes compst)))))