let disapply (x, y) a =
  try
    (match d_interp a with
       | Sym.Apply, [c; a1; a2; _; b] when is_c c ->
           if Term.eq x a1 && Term.eq y a2
             || Term.eq x a2 && Term.eq y a1 
           then
             b
           else 
             a
       | _ ->
           a)
  with
      Not_found -> a