(atj-restore-and-calls-in-terms terms) → new-terms
Theorem: len-of-atj-restore-and-calls-in-terms
(defthm len-of-atj-restore-and-calls-in-terms (b* ((?new-terms (atj-restore-and-calls-in-terms terms))) (equal (len new-terms) (len terms))))