If a variable is in scope for the old code, its renamed counterpart is in scope for the new code.
Theorem:
(defthm check-var-when-var-renamevar (implies (and (not (reserrp (var-renamevar old new ren))) (check-var old (varset-old ren))) (check-var new (varset-new ren))))