[PVS-HELP] Datatype subtype problem

["fsong" <fsong@xxxxxxxxxxxxxxx>]

Dear Everyone:

I define a theory which contain a Datatype like is:

Expr [Vars,Value: TYPE+]: THEORY
BEGIN
  IMPORTING env[Vars,Value]
  Expr_terms:  TYPE=[Env->Value]
  Bexpr_terms: TYPE=[Env->bool]
 
  rhs :DATATYPE WITH SUBTYPES Vars,Expr_terms,Value
  BEGIN
    expression(e: Expr_terms)      :expr?          : Expr_terms
    variable(v: Vars)              :va?            : Vars
    constant(v: Value)             :con?           : Value
  END rhs
END Expr

Then I want to declare 
  x,y   :Vars
  v1    :[Vars,rhs] =(x,y) 
it is error in y, the type is not match . But I have declared "Vars" is subtype of rhs.

Is anyone know what`s wrong.