lean: add match equation binders for termination measures

[nek0las]

This aims to solve issue #1659, where Lean 4 cannot automatically find the equality between variables. We add a hypothesis to the match expression so the termination checker can use it.

For example, the generated Lean code now includes h_match in the match expression:

  /-- Type quantifiers: arg1 : Int, arg0 : Int -/
  def test (arg0 : Int) (arg1 : Int) : Bool :=
    let merge_var := (arg0, arg1)
    match h_match : merge_var with
    | (0, g__0) => false
    | (1, x) => (x >b 5)
    | (x, y) =>
      (if ((x ≤b 0) : Bool)
      then false
      else (test (x -i 1) (x +i y)))
  termination_by (let merge_var := (arg0, arg1)
  let (x, _) := merge_var
  x).toNat