[PVS-Help] nonempty type tcc

[robert <robert@itee.uq.edu.au>]

I've just changed to version 3.2 and a problem has cropped up.

I have a theory

proc: THEORY
begin
    PROC: TYPE+
end proc

I import this theory via library, eg, 

sq_abstract: THEORY
BEGIN
	
	lib: LIBRARY = "whatever"

	importing lib@proc

	.....

	pp: PROC

	.....
end sq_abstract

The type checker generates the tcc 

% Existence TCC generated (at line 97, column 1) for  pp: PROC
  % unfinished
pp_TCC1: OBLIGATION EXISTS (x: PROC): TRUE;

This isn't proved when I use M-x prove-tccs-theory (ie, using (tcc)
or (grind)).

I introduced a theorem identical to pp_TCC1 in theory proc and was able 
to prove it straight away using (grind).

How can I prove it as an obligation?

Thanks,
Rob