feat: adapt non-equality theorems in `mkTheoremFromDecl` (#13041)

This PR extends `mkTheoremFromDecl` and `mkTheoremFromExpr` to handle
theorems whose conclusion is not an equality, enabling `Sym.simp` to use
a broader class of lemmas as rewrite rules.

Adaptations:
- `¬ p` → `p = False` via `eq_false`
- `p ↔ q` → `p = q` via `propext`
- `p` (proposition) → `p = True` via `eq_true`

Conjunctions (`p ∧ q`) are not handled here since the `SymM` E-graph
aggressively splits them via case analysis.

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>