This PR fixes an issue in the elaborator where delayed substitutions involving dependent let bindings could create type-incorrect terms. To address this, we encode the let value into the type of the metavariable involved in the delayed substitution, which is then checkable by Meta.check or rewriting tactics.

Implementation: it adds a defeqParam parameter gadget that is only meant to be used for metavariables created by the MetavarContext system when a metavariable depends on a dependent let that is being abstracted. In Meta.check, there is an additional check for applications that if the domain has @defeqParam t v then the argument is definitionally equal to v. This immediately fixes any tactic (like rw or clear_value) that uses Meta.check in its operation.

For example, after elaborating (let v := n + 1; ?m : Nat), we get a metavariable ?d and the expression let v := n + 1; ?d v, with a delayed assignment ?m := ?d v. Before this PR, the type of ?d was ?d : Nat -> Nat, but now it is ?d : defeqParam (n + 1) -> Nat. This defeqParam (n + 1) gadget is definitionally equal to Nat, but Meta.check will ensure the argument to ?d is definitionally equal to n + 1. If we were to zeta reduce the expression, we'd get ?d (n + 1), which is still type correct according to Meta.check. Trying to rewrite with Nat.add_comm will fail, since the motive needs to be ?d a for an abstract a : Nat, which is not definitionally equal to n + 1.

Note: This gadget is not meant to be used by users. It is only for the implementation of delayed assignments. It is also not part of Lean's type theory, since it is merely a hint used by the elaborator.

Closes #8488