 where t is a placeholder for singular terms in general (including parameters), and not just for @-terms. The right-hand side may contain occurrences of @; moreover, when taking instances, expressions substituted for either F or t may contain occurrences of @. And all that is important with a single-abstraction identity principle is whether the theory in question contains it as a theorem (or theorem-scheme). 