 A proof is any finite sequence of formulas, each of which is an axiom or an immediate consequence, by a rule of inference, of (one or two) preceding formulas of the sequence. Any proof is said to prove its last formula, which is called a theorem or provable formula of first-order intuitionistic predicate logic. A derivation of a formula \(E\) from a collection \(F\) of assumptions is any sequence of formulas, each of which belongs to \(F\) or is an axiom or an immediate consequence, by a rule of inference, of preceding formulas of the sequence, such that \(E\) is the last formula of the sequence. If such a derivation exists, we say \(E\) is derivable from \(F.\) 