let mapargs mk_app f a =
    let (op, al) = Term.App.destruct a in
      match al with
        | [] -> 
            id a
        | [a1] ->
            let (b1, rho1) = f op a1 in
              if a1 == b1 then id a else 
                let (b, tau) = mk_app op [b1] in
                  (b, dep2 tau rho1)
        | _ ->
            let rho = ref dep0 in                (* [rhoi |- bi = ai] *)
            let f' a = 
              let (b, rhoi) = f op a in
                rho := dep2 rhoi !rho; b
            in
            let bl = Term.mapl f' al in                                
              if al == bl then id a else 
                let (b, tau) = mk_app op bl in   (* [tau |- b = op(bl)] *)
                  (b, dep2 tau !rho)