decide +kernel rejects goals with a variable type; use mkAuxTheorem with Eq.refl

In a reflective tactic over a generic structure (e.g. {K} [Field K] [LinearOrder K]), the certificate goal φ.check = true mentions the fvars K and its instances, so decide +kernel fails with 'Expected type must not contain free variables' (+revert does not help, since ∀ K inst, ... is not Decidable). Fix (Lean v4.35): let h ← mkAuxTheorem (← mkEq lhs (mkConst Bool.true)) (mkApp2 (mkConst Eq.refl [1]) (mkConst Bool) (mkConst Bool.true)). mkAuxTheorem abstracts the fvars itself and adds the closed lemma, so the kernel evaluates check under binders, which is fine as long as the computation never inspects K-valued data. Wrap it in try/catch: a false certificate surfaces as a kernel error at that point, not later at the declaration.