feat: adapt non-equality theorems in `mkTheoremFromDecl`

`mkTheoremFromDecl` and `mkTheoremFromExpr` now handle theorems whose
conclusion is not an equality:
- `¬ p` → adapted to `p = False` via `eq_false`
- `p ↔ q` → adapted to `p = q` via `propext`
- `p` (proposition) → adapted to `p = True` via `eq_true`

This enables `Sym.simp` to use hypotheses like `h : p x` as rewrite
rules that replace `p x` with `True`.

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