The word "instantiation" is used in Ivy to refer to several different things:

• "schema instantiation" as a form of judgment application within a proof
• explicit quantifier instantiation within a proof
• module instantiation that declares an object within a module
• theory instantiation that declares an interpretation of a type within a module