let rec replace v s =
  let rec repl a = 
    match a with
      | Var _ ->
          v (find s a)
      | App(f, al) ->
          let al' = Term.mapl repl al in
          let a' = if al == al' then a else Th.sigma f al' in
            find s a'
  in
    repl