A First-Order Logic of Proofs, \(\textsf{FOLP}\), with quantifiers over individual variables, has been presented in Artemov and Yavorskaya (Sidon) (2011). In \(\textsf{FOLP}\) proof assertions are represented by formulas of the form \(t{:}_X A\) where \(X\) is a finite set of individual variables that are considered global parameters open for substitution. All occurrences of variables from \(X\) that are free in \(A\) are also free in \(t{:}_X A\). All other free variables of \(A\) are considered local and hence bound in \(t{:}_X A\). For example, if \(A(x,y)\) is an atomic formula, then in \(p{:}_{\{x\}} A(x,y)\) variable \(x\) is free and variable \(y\) is bound. Likewise, in \(p{:}_{\{x,y\}} A(x,y)\) both variables are free, and in \(p{:}_{\emptyset} A(x,y)\) neither \(x\) nor \(y\) is free.