feat: add `backward.isDefEq.implicitBump` option

This PR adds the `backward.isDefEq.implicitBump` option (default: `false`)
that controls whether all implicit arguments get their transparency bumped
to `TransparencyMode.instances` during `isDefEq`, not just instance-implicit
ones. When enabled, `[implicit_reducible]` definitions like `Nat.add` and
`Array.size` are unfolded when checking implicit arguments, closing the gap
between instance-implicit and regular implicit argument handling.

The default is `false` for staging purposes. After stage0 is updated, the
default will be flipped to `true`.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>