Disable automatic deduction of motive like arguments

Stream: lean4

[Leni Aniva]

Consider this example:

example: ∀ (n: Nat), n + 0 = n := by
  intro n
  apply Nat.brecOn

This fills in the motive as fun t => n + 0 = t which is obviously wrong. Is there a way to disable this behaviour at the MetaM level? In general the behaviour I want is that if isDefEq is unifying ?m1 ?m2 with x, it should leave ?m1 and ?m2 untouched because there could be multiple potential solutions.