Rules about var-autop.
These serve to discharge the var-autop hypothesis
in rule
Theorem:
(defthm var-autop-of-add-frame (not (var-autop var (add-frame fun compst))))
Theorem:
(defthm var-autop-of-enter-scope (equal (var-autop var (enter-scope compst)) (var-autop var compst)))
Theorem:
(defthm var-autop-of-add-var (equal (var-autop var (add-var var2 val compst)) (or (equal (ident-fix var) (ident-fix var2)) (var-autop var compst))))
Theorem:
(defthm var-autop-of-update-var (equal (var-autop var (update-var var2 val compst)) (var-autop var compst)))
Theorem:
(defthm var-autop-of-update-static-var (equal (var-autop var (update-static-var var2 val compst)) (var-autop var compst)))
Theorem:
(defthm var-autop-of-update-object (equal (var-autop var (update-object objdes obj compst)) (var-autop var compst)))