 The corresponding introduction rule is less obvious: the domain might be infinite, and only finitely many conjuncts can occur in a formal proof! We proceed more circuitously. First, we assume an “alphabet” of special terms (variously called free variables, parameters, dummy constants,…). Next, we define a special sort of subproof, the subproof general with respect to a particular term from this alphabet: in Fitch’s notation, these subproofs are marked with an occurrence of the relevant term beside the top of its vertical line. These subproofs are subject to a restriction on reiteration: a formula containing a particular one of the special terms cannot be reiterated into a subproof general with respect to that term. Then we may state the rule