feat: assert non-indexable ground theorems as facts in `grind` parameters

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.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>