Do not substitute through a capturing quantifier binder

[Chessing234]

Summary

• searchReplace walked into ∀/∃ binders, so replacing X could rename the bound variable.
• Nested quantifiers that bind the search term now skip the body (shadowing). Binders are left alone.
• subs accepts term-context templates instead of erroring.

Test plan

• Universal/existential instantiation still rewrites the matrix, not the binder
• Substituting a free X into a formula that contains ∀X leaves the inner binder and its body