The constraint resulting from this proof
Formulae that are introduced into the antecedent by this rule application (one set for each subproof).
Formulae that the proof assumes to be present on this branch (i.e., premisses of rules applied in the proof).
Set of constants occurring in this certificate.
Constants bound by the root operator of the certificate.