def sacha : Nat :=
  let (v, k) := match 0 with
    | (n) => (0, 0)
  v + k