[PVS-Help] extend

[Jerome White <jerome@xxxxxxxxxxxxxx>]

I have the following definition:

  S, A, T: TYPE
  f: FUNCTION[S, set[A] -> T]
  % ...
  unchanged?(pre, post: S, K: set[A]): bool =
    FORALL (k: (K)): f(pre, singleton(k)) = f(post, singleton(k))

When 'unchanged?' is opened in a proof, I get the following:

  [1]   unchanged?(pre!1, post!1, complement(add(t!1, B!1)))
  Rule? (rewrite "unchanged?")
  {1}   FORALL (j: (complement(add(t!1, B!1)))):
	f(pre!1,
	    extend[A, (complement(add(t!1, B!1))), bool, FALSE]
		(singleton(j)))
	   =
	   f(post!1,
	     extend[A, (complement(add(t!1, B!1))), bool, FALSE]
		       (singleton(j)))

What exactly is 'extend'? I see it in the prelude, but am unsure of
what it means in this context and why it's popping up. Any insight
would be much appreciated. Thanks

jerome