grind failed to create local e-matching theorem

Stream: lean4

[Christian Merten]

The following yields failed to create E-match local theorem (on both latest mathlib and nightly):

example (p : Nat → Prop) (h : ∀ n : Nat, p n) : p 42 := by
  -- abstract predicate: succeeds
  grind

example (h : ∀ n : Nat, n = 3) : 42 = 3 := by
  /- fails with
  [grind] Issues ▼
  [issue] failed to create E-match local theorem for
        ∀ (n : Nat), n = 3
  -/
  grind

In the abstract predicate case, grind succeeds, but when the abstract predicate is replaced by something concrete it fails. Is this expected?

[Kim Morrison]

Yes. :-)