Instance of an inference rule

A specific substitution of the rule's Metavariables with concrete terms, yielding a particular Derivation step.