 Here 1, 2 and 5 are axioms; 4 comes from 2 and 3 by modus ponens; and 6 and 7 come from earlier lines by modus ponens; so no variables have been varied. The Deduction Theorem tells us there is a proof \(P\) in \(\mathbf{H–IQC}\) of \(A(x) \rightarrow \neg \forall\)x\(\neg A(x),\) and one application of \(\exists\)-elimination converts \(P\) into a proof of \(\exists x A(x) \rightarrow \neg \forall x\neg A(x).\) The converse is not provable in \(\mathbf{H–IQC},\) as shown in Section 5.1 below.