refactor: reorganize SymM and GrindM monad hierarchy

[leodemoura]

This PR reorganizes the monad hierarchy for symbolic computation in Lean.

Motivation

We want a clean layering where:

1. A foundational monad (SymM) provides maximally shared terms and structural/syntactic isDefEq
2. GrindM builds on this foundation, adding E-graphs, congruence closure, and decision procedures
3. Symbolic execution / VCGen uses GrindM directly without introducing a third monad

Changes

The core symbolic computation layer still lives in Lean.Meta.Sym. This monad (SymM) provides:

• Maximally shared terms with pointer-based equality
• Structural/syntactic isDefEq and matching (no reduction, predictable cost)
• Monotonic local contexts (no revert or clear), enabling O(1) metavariable validation
• Efficient intro, apply, and simp implementations

The name "Sym" reflects that this is infrastructure for symbolic computation: symbolic simulation, verification condition generation, and decision procedures.

Updated hierarchy

Lean.Meta.Sym   -- SymM: shared terms, syntactic isDefEq, intro, apply, simp
Lean.Meta.Grind -- GrindM: E-graphs, congruence closure (extends SymM)

Symbolic execution is a usage pattern of GrindM operating on Grind.Goal, not a separate monad. This keeps the API surface minimal: users learn two monads, and VCGen is "how you use GrindM" (for users that want to use grind) rather than a third abstraction to understand.