Defines variants of `have`

and `let`

syntax which do not produce `let_fun`

or `let`

bindings,
but instead inline the value instead.

This is useful to declare local instances and proofs in theorem statements and subgoals, where the extra binding is inconvenient.

`haveI`

behaves like `have`

, but inlines the value instead of producing a `let_fun`

term.

## Equations

- One or more equations did not get rendered due to their size.

`letI`

behaves like `let`

, but inlines the value instead of producing a `let_fun`

term.

## Equations

- One or more equations did not get rendered due to their size.

`haveI`

behaves like `have`

, but inlines the value instead of producing a `let_fun`

term.

## Equations

- One or more equations did not get rendered due to their size.

`letI`

behaves like `let`

, but inlines the value instead of producing a `let_fun`

term.

## Equations

- One or more equations did not get rendered due to their size.