 Much less is known about the admissible rules of intuitionistic predicate logic. Pure \(\mathbf{IQC},\) without individual or predicate constants, has the following remarkable admissible rule for \(A(x)\) with no variables free but \(x\):