[PVS-Help] singleton_elt

[Jerome White <jerome@xxxxxxxxxxxxxx>]

I have the following theory:

   example[T: TYPE, f: FUNCTION[T -> T]]: THEORY
   BEGIN
     IMPORTING operator_defs_ext[T]
     g(a, b: T): T = f(union(a, b))

     ident: LEMMA identity?(g)(emptyset)
   END example

When proving 'ident' I am presented with the following:

     |-------
   {1}   identity?(g)(singleton_elt[T](emptyset))

Why is the 'singleton_elt[T]' popping up? Thanks

jerome