If two (lists of) paths are related by variable renaming, the safety of the old one implies the safety of the new one.
Theorem:
(defthm check-safe-path-when-path-renamevar (implies (not (reserrp (path-renamevar old new ren))) (b* ((ok-old (check-safe-path old (varset-old ren))) (ok-new (check-safe-path new (varset-new ren)))) (implies (not (reserrp ok-old)) (not (reserrp ok-new))))))
Theorem:
(defthm check-safe-path-list-when-path-list-renamevar (implies (not (reserrp (path-list-renamevar old new ren))) (b* ((ok-old (check-safe-path-list old (varset-old ren))) (ok-new (check-safe-path-list new (varset-new ren)))) (implies (not (reserrp ok-old)) (not (reserrp ok-new))))))