Universal instantiation is a rule of inference for several predicate logics that allows one to substitute any term for a variable bound with the universal quantifier, while removing the quantifier. In symbols: where is any term (such as a variable, function symbol, or a constant).