[PVS-Help] choose problem

["fsong" <fsong@xxxxxxxxxxxxxxx>]

Dear everyone:

Env: TYPE =[Env->Value]
trans: TYPE ={Env->Env]
f,g: Var trans
init_env:   Env

<<(env1:VarEnv,env2:VarEnv): bool= FORALL (x:Vars): env1(x)=env2(x)

c(f,g): trans=trans = LAMBDA (s: Env): choose({y: VarEnv|y<<f(s) or y<<g(s)}) 

how can I to proof the nonemptyness of {y: VarEnv|y<<f(s) or y<<g(s)}???

I try to proof the law c(f,g)(init_env) = c(g,f)(init_env)
the proof tree as follow.

L1 :  

  |-------
{1}   FORALL (f, g: trans[Vars, Value]):
        c(f, g)(Init_env) = c(g, f)(Init_env)

Rule? (skolem!)
Skolemizing,
this simplifies to: 
L1 :  

  |-------
{1}   c(f!1, g!1)(Init_env) = c(g!1, f!1)(Init_env)

Rule? (expand "c")
Expanding the definition of c,
this simplifies to: 
L1 :  

  |-------
{1}   choose({y: VarEnv | y << f!1(Init_env) OR y << g!1(Init_env)}) =
       choose({y: VarEnv | y << g!1(Init_env) OR y << f!1(Init_env)}

then I do not know how to proof this issue, if  it is not hold?

how can I represent the choice(f,g) in PVS?

Thanks
Song