FTY utilities for pseudo-terms.

Many system utilities, e.g. built-in and in Std/system, are written using the built-in ACL2 term API.
When using these system utilities
in code that uses the FTY term API, there may be a slight ``mismatch'',
e.g. in the way the two APIs fix non-terms,
or in the fact that, for termination,
the ACL2 API is based on `ACL2-count`
while the FTY API is based on `pseudo-term-count`.

The mismatch can be bridged by introducing simple wrappers of those system utilities that fix the term (in the FTY way) and then call the utilities. Here we provide a number of such wrappers, which should be eventually moved to a more central place.

The wrappers are accompanied by theorems leveraged from the wrapped utilities. This way the wrappers can be left disabled in code that uses them.

The `ACL2-count` vs. `pseudo-term-count` issue
requires a bit more work.
Suppose we have a utility that returns results
that are `ACL2-count`-smaller than its arguments
(under suitable conditions).
In order to prove that the wrapper returns results
that are `pseudo-term-count`-smaller than its arguments,
we cannot leverage the theorems about `ACL2-count`.
Instead, we need to enable the utilities to prove the theorems,
and we also need to enable some FTY pseudo-term operations,
because we need to break the FTY pseudo-term abstraction:
we use this approach to prove theorems
about the original utilities and `pseudo-term-count`
under `pseudo-termp` assumptions,
from which then the desired theorems about the wrappers readily follow.
The theorems about the original utilities and `pseudo-term-count`
are useful to prove the analogous theorems of utilities that call them.

- Fty-check-mv-let-call
- FTY version of
`check-mv-let-call`. - Fty-check-lambda-call
- FTY version of
`check-lambda-call`. - Fty-check-if-call
- FTY version of
`check-if-call`. - Fty-remove-equal-formals-actuals
- FTY version of
`remove-equal-formals-actuals`. - Fty-check-and-call
- FTY version of
`check-and-call`. - Fty-check-or-call
- FTY version of
`check-or-call`. - Fty-check-fn-call
- FTY version of
`check-fn-call`. - Fty-check-not-call
- FTY version of
`check-not-call`. - Fty-check-list-call
- FTY version of
`check-list-call`. - Fty-fsublis-var-lst
- FTY version of
`fsublis-var-lst`. - Fty-if-to-if*
- Replace each
`if`with`if*`in a term. - Fty-fsublis-var
- FTY version of
`fsublis-var`.