More questions about predicate subtypes

[Kellom{ki Pertti <pk@cs.tut.fi>]

I have some more questions about predicate subtypes. What I am trying
to do is to use predicate subtypes to constrain more than one argument
of a function. The following theory hopefully illustrates what I am
doing:

test: THEORY
 BEGIN
  obj: TYPE+
  t: TYPE+
  p: [obj, t -> bool]
  i: [(p) -> int]
  f: [(p) -> int] = LAMBDA (x: obj, st: t): i(x, st) + 1
  g(x: obj, st: (LAMBDA (s: t): p(x, s))): int = i(x, st) + 1
 END test

I am trying to express a function of type [(p) -> int]. I would prefer
the form in which f is written, but I get a TCC

  f_TCC1: OBLIGATION FORALL (st: t, x: obj): p(x, st);

and I do not know how to get to the type information that says that
p(x,st) is true. Skolemizing and doing (typepred "(x!1, st!1)") does
not work.

For g I get the TCC 

  g_TCC1: OBLIGATION FORALL (x: obj, st: (LAMBDA (s: t): p(x, s))): p(x, st);

which is provable.

My questions now are:
   - Can f_TCC1 be proved?
   - Is restricting the last argument using dependent types as in g 
     completely equivalent to giving the restriction as in the
     declaration of f?

Thanks,
	Pertti