[Agda] mutual recursion on vectors?

[Kenichi Asai]

One can easily write a function that recurse over a natural number:

f1 : ℕ → ℕ
f1 zero = zero
f1 (suc x) = f1 x

Given an argument m, it returns zero after m recursive calls.  For two
argument function, one can define:

mutual
  f2a : ℕ → ℕ → ℕ
  f2a zero zero = zero
  f2a zero (suc y) = f2b zero y
  f2a (suc x) y = f2a x y

  f2b : ℕ → ℕ → ℕ
  f2b zero zero = zero
  f2b (suc x) zero = f2a x zero
  f2b x (suc y) = f2b x y

where f2a is called recursively when its first argument decreases
(with the second argument unchanged), and f2b is called recursively
when its second argument decreases (with the first argument unchanged).
Given arguments m1 and m2, it returns zero after m1+m2 recursive calls.

Can I generalize this to n argument case?

fn : {n : ℕ} → (index : Fin n) → Vec ℕ n → ℕ
fn {n} index v = {!!}

Namely, given an index and a vector of n numbers, it defines n
functions mutually recursively.  fn i will be called recursively when
its ith argument decreases (with all the other arguments unchanged).
Given a vector of n numbers, m0, ..., m_{n-1}, it returns zero after
m0 + ...  + m_{n-1} recursive calls.

It appears I can define it by adding an extra argument keeping the
sum of all the numbers.  But then I lose the mutual recursive
structure: even if sum is not zero, I don't know which of the n
numbers is non zero, and even I have to have the case where all the
numbers are zero, which can't happen if sum is zero.

Sincerely,

-- 
Kenichi Asai