[TYPES] A doubt in AUTOMATH type system

[Param Jyothi Reddy]

Hi,
I am trying to understand how automath lines could be interpreted in
PTS. in this regard i got stuck at the following. Any help would be
appreciated.

Can someone help me understand the meaning of p:PROP in the following Line:
@[sigma:TYPE][p:[x:sigma]PROP]
l_all:=p:PROP

in the paramters we have said that p:[x:Sigma]PROP. So how can p be
type fo PROP.

It is used as follows:
@[sigma:TYPE][p:[x:sigma]PROP][a1:l_all(sigma,p)][s:sigma]
l_alle:=<s>a1:<s>p

If i interpret paramters in definition of l_all as lambda then
l_all(sigma, p) reduces to p hence disallowing a1 : l_all(sigma, p).
Interpreting paramters as product is not possible because the body is
not correctly typed.

Regards,
Param