[BUG] REPL accepts incorrect proofs

I found a peculiar bug in REPL, where it can accept any proof that applies the theorem itself.

Example:

{"cmd": "theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by sorry"}

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 1, "column": 62},
   "goal": "p q : Prop\nhp : p\nhq : q\n⊢ p ∧ q ∧ p",
   "endPos": {"line": 1, "column": 67}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 1, "column": 8},
   "endPos": {"line": 1, "column": 12},
   "data": "declaration uses 'sorry'"}],
 "env": 0}

{"tactic": "apply test", "proofState": 0}

{"proofState": 1,
 "goals":
 ["case hp\np q : Prop\nhp : p\nhq : q\n⊢ p",
  "case hq\np q : Prop\nhp : p\nhq : q\n⊢ q"]}

In the above example, we cannot complete the proof by applying itself. However, REPL does not raise any error messages. However, on VS Code IDE for Lean 4, we get the error message for the proof below:

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
    apply test
    exact hp
    exact hq

Expected Error message:

fail to show termination for
  Lean4Proj1.test
with errors
structural recursion cannot be used

Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
          hp hq
1) 5:8-12  _  _
Please use `termination_by` to specify a decreasing measure.

Start by reproducing the JSON REPL exchange in the issue and compare its result with the Lean 4 VS Code behavior shown there. Trace how the REPL handles applying the theorem itself and ensure the invalid recursive proof produces the expected termination error.