[PVS-Help] Parametrized type equivalence

["Gabor Guta" <Gabor.Guta@xxxxxxxxxxxxxxxxxxx>]

Dear PVS Developers/Users,

   I have a question respect to the parametrization of types.

There are two theories:

A[T: TYPE] defines a type called AT which depends on T

B[T: TYPE]: THEORY
BEGIN
IMPORTING A
a1: VAR AT
a2: VAR AT[T]
...
END B

Are the types of the of a1 and a2 variables equivalent? I think, yes;
...because a2 is an instance of AT with parameter T, but in the end both
of the variables are "generic" having a parameter T:TYPE. Can somebody
confirm this assumption?

Thank you very much!

Regards, Gabor