feat: assert non-indexable ground theorems as facts in `grind` parameters (#15609)

This PR makes `grind [mkP]` accept a theorem whose statement is not a
`∀` and is not indexable, e.g., `theorem mkP : P` for a nullary
inductive predicate `P`. The parameter is asserted as a fact, so the
workaround `grind [(mkP)]` is no longer needed. `grind?` and `finish?`
keep such identifiers in their suggestions.

Previously, identifier parameters always went through E-matching theorem
construction, which fails for `mkP` since only applications can serve as
patterns. The new helper `isFactDecl` detects this case. Indexable
ground theorems such as `pi_pos : 0 < π` are unaffected.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>