citp init

:init [as <name>] { "[" <label> "]" | "(" <sentence> "")} by "{" <variable> <- <term>; ... "}"

Instantiates an equation specified by <label> by replacing the <variable>s in the equation with the respective <term>s. The resulting equation is added to the set of axioms. If optional as <name> is given, label of the instantiated axiom is overwritten by .

Related: citp