 The sequents above a rule’s line are called the rule’s premises and the sequent below the line is the rule’s conclusion. The quantification rules ∃→ and →∀ have an eigenvariable condition that restricts their applicability, namely that a must not occur in Γ, Δ or in the quantified sentence. The purpose of this restriction is to ensure that the choice of parameter, a, used in the substitution process is completely “arbitrary”.