let d_add = function
  | Term.App((Sym.Arith(Sym.Add), _), al, _) -> al
  | _ -> raise Not_found