let map ctxt a = match a with | Var _ -> ctxt(a) | App(f, l, _) -> let l' = Term.mapl ctxt l in if l == l' then a else Term.App.mk_app f l'