Proofs (justifications) are represented by proof terms which do not contain individual variables. In addition to \(\textsf{LP}\) operations there is one more series of operations on proof terms, \({\sf gen}_x(t)\), corresponding to generalization over individual variable \(x\). The new axiom that governs this operation is \(t{:}_X A {\rightarrow}{\sf gen{:}_x(t)}_X\forall x A\), with \(x\not\in X\). The complete list of \(\textsf{FOLP}\) principles along with realization of First-Order \(\textsf{S4}\) can be found in Artemov and Yavorskaya (Sidon) (2011). A semantics for \(\textsf{FOLP}\) has been developed in Fitting (2014a).