let d_add = function
  | App(Arith(Add), xl) -> Some(xl)
  | _ -> None