# Second-order-theorem-instances

Notion of instance of a second-order theorem.

An instance of a second-order theorem is an ACL2 theorem
introduced via `defthm-inst`,
which replaces function variables that the second-order theorem depends on
with functions of matching arities.
This macro specifies the replacement as an
instantiation,
which is applied to the formula of the second-order theorem.

The new theorem is second-order if it still depends on function variables,
otherwise it is first-order.
`defthm-inst` generates a proof for the new theorem
that uses a functional
instance of the second-order theorem that is being instantiated.

### Subtopics

- Defthm-inst
- Introduce a theorem by instantiating a second-order theorem.