[PVS-Help] rewriting add_as_union

[Jerome <jerome@xxxxxxxxxxxxxx>]

I'm trying to use the rewrite rule to get the following ([1]) to
simplify:

  [-1]  disjoint?(singleton(e!1), L!1)
    |-------
  [1]   fun(s!1, (union(singleton(e!1), L!1))) = s!1(e!1) o fun(s!1, L!1)

  Rule? (rewrite "add_as_union" :dir RL)
  No matching instance for add_as_union found.
  No change on: (REWRITE "add_as_union" :DIR RL)
  disjoint_compose.1 :

  [-1]  disjoint?(singleton(e!1), L!1)
    |-------
  [1]   fun(s!1, (union(singleton(e!1), L!1))) = s!1(e!1) o fun(s!1, L!1)

where 'add_as_union' is defined in the prelude to be:

  add(x, a) = union(a, singleton(x))

Is this problem due to the fact that the singleton and set definitions
in my consequent are opposite to those in prelude? Is there anyway to
use rewrite (or even rewrite-lemma) to get this to work? Thanks

jerome