let result_type tenv t = 
  let a = symbol tenv (TName "->") in
  let rec chop n t = 
    if n = 0 then t 
    else 
      match t with
        | TTerm (App (TTerm (App (v, t)), u)) when v = a -> chop (n-1) u
        | u -> assert (n <= 0); u
  in
    chop (-1) t