test: expect the InLean kernel's behaviour

The kernel reports its errors as `Kernel.Exception.other "(InLean) …"`, so the tests that compare kernel error text expect that text; where InLean's message differs from the C++ kernel's (e.g. a type mismatch in `12520_1`, projections of indexed structure-like types, which the kernel declines in `inductive_rec_proj`), the tests expect InLean's.

* `issue14484`: the error of `assumptionFreeFalse` is now shown: the C++ kernel's message mentioned the synthetic `sorry` in the axiom's type and was filtered, InLean's text does not.
* `10475`: `Kernel.check` substitutes the `let` values in the inferred type, so the types are `True` and `Prop`; the second check succeeds as the issue requires.
* `grind_nestedDecidable_kernel_issue` also checks its regular-wrapper control.
* `completion7` and `completionEOF` declare their own `And` in a `prelude` file; InLean reserves the names of the basis blocks it pins, so they use `Duo` (the same length, so the positions stay).
* `kernelQuotNameCollision` is deleted: it declares an axiom at `Quot.lift` before `init_quot` and expects the quotient declaration to be rejected; InLean reserves the quotient's names and rejects the axiom itself, so that situation cannot arise.
* `inleanQuotTwice` (new) checks that a second quotient declaration is a no-op.
* The `leanchecker` and `module` package tests expect the new messages.

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