[PVS-Help] Explicating dependent types

[Aditya Kanade <aditya@cse.iitb.ac.in>]

Hi,

Suppose we define a record consisting of a set 's' and a set 'f' over 
pairs of elements from the set. If a pair (p,q) belongs to f then 
clearly p and  q should belong to s by the dependent typing. I encouter 
a similar kind of proof goal which I'm not able to prove. 'typepred' 
does not change state of the proof goal. Below I'm giving a small 
example theory capturing essence of the problem. The lemma 'l' below 
could not be proven. Rather, PVS generates a TCC saying p and q should 
be of the type r`s.

TH:theory
begin
T:type

R:type = [# s:set[T], f:set[[(s),(s)]] #]

l:lemma
forall (r:R): forall (p,q:T): r`f(p,q) implies r`s(p) and r`(q)

end TH

How does one explicate the dependent typing information?

Regard,
Aditya.