feat: improve `instantiateExtTheorem` in `grind`

This PR leverages the fact that expressions are type correct in
`grind` and the conclusion of extensionality theorems is of the form
`?a = ?b`.

This PR is relevant for #12179 because it enables us to use a weaker
`isDefEq` that does not bump the transparency level when processing
implicit arguments.