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)