Consider formulas $A$ of predicate calculus such that no variables can be bound and free for $A$ at the same time. Term $t$ is said to be free for $x$ in $A$ if $x\notin FV(A)$ or no variables of $t$ appears in $A$ as bound ones. Lets generalise the notion of a subformula: we say that $[A]_t^x$ is a generalised subformula of $\textbf{Q}xA,\:\textbf{Q}\in\{\forall,\exists\},$ if the term $t$ is free for $x$ in A.
Prove that if $B$ is a proper generalised subformula of $\textbf{Q}xA$ where $\textbf{Q}$ is a quantifier then there exists a term $t$ free for $x$ in $A$ such that $B$ is a generalised subformula of $[A]_t^x$.
Intuitively this statement is evident but I am not pretty sure about a formal proof. I've tried to use induction (the base is trivial) but I don't know how exactly must the step look like.
Maybe I overcomplicate and all needed to be said is: if required $t$ does not exist then $B$ is not a generalised subformula for any of $[A]_t^x$ and, hence, it must be the whole $\textbf{Q}xA$ but $B$ is proper. Contradiction.
I am not sure. What can you say?