 The soundness of such a rule is easy to see. The restriction on reiteration into general subproofs means that no special assumptions on the term \(a\) can be smuggled into a subproof general with respect to \(a\). The subproof, therefore, can be seen as displaying a schema by which (pretending for the moment that every element in the domain has a  name[17])  proofs could be constructed of an instance of the quantification for each element.