Extend the #decompose command to accept arbitrary expressions (wrapped in
parentheses) on the RHS of clauses, in addition to identifiers.

When an identifier is provided (existing behavior), #decompose creates a new
auxiliary definition (or reuses an existing one). When an expression is
provided, #decompose checks that it is definitionally equal to the extracted
sub-expression and uses it directly in the rewrite theorem.

Example:
  def add_mul (y x : U32) := do
    let x ← x + y
    x * 2#u32

  #decompose f f_eq
    letRange 0 2 => (add_mul 1#u32)
    letRange 1 2 => (add_mul 2#u32)

  -- f_eq : f x = do
  --   let x ← add_mul 1#u32 x
  --   let x ← add_mul 2#u32 x
  --   ...

Closes #1109

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Replace the parenthesized expression syntax with a uniform comma-terminated
syntax for all clause RHS:

  -- Before (identifier only):
  #decompose f f_eq
    letRange 0 2 => f_prefix

  -- Before (expression, parenthesized):
  #decompose f f_eq
    letRange 0 2 => (add_mul 1#u32)

  -- After (uniform, comma-terminated):
  #decompose f f_eq
    letRange 0 2 => f_prefix,
    letRange 0 2 => add_mul 1#u32,

The comma delimits the end of the term. If the RHS is a single unresolved
identifier, a new definition is created (existing behavior). Otherwise the
RHS is elaborated as an expression and checked for definitional equality.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>