Try to close goal using `rfl`

with smart unfolding turned off.

## Equations

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

## Instances For

Returns the "const unfold" theorem (`f.eq_unfold`

) for the given declaration.
This is not extensible, and always builds on the unfold theorem (`f.eq_def`

).

## Equations

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