 It is important to note that, in the definition of a derivation from assumptions in \(\mathbf{H–IQC},\) the assumption formulas are treated as if all their free variables were universally quantified, so that \(\forall x A(x)\) is derivable from the hypothesis \(A(x).\) However, the variable \(x\) will be varied (not held constant) in that derivation, by use of the rule of \(\forall\)-introduction; and so the Deduction Theorem cannot be used to conclude (falsely) that \(A(x) \rightarrow \forall x A(x)\) (and hence, by \(\exists\)-elimination, \(\exists x A(x) \rightarrow \forall x A(x))\) are provable in \(\mathbf{H–IQC}.\) As an example of a correct use of the Deduction Theorem for predicate logic, consider the implication \(\exists x A(x) \rightarrow \neg \forall x\neg A(x).\) To show this is provable in \(\mathbf{H–IQC},\) we first derive \(\neg \forall x\neg A(x)\) from \(A(x)\) with all free variables held constant: