(fty-if-to-if*-lst terms) → terms1
Theorem: len-of-fty-if-to-if*-lst
(defthm len-of-fty-if-to-if*-lst (b* ((?terms1 (fty-if-to-if*-lst terms))) (equal (len terms1) (len terms))))