# what's the precise meaning of ...?

Hello, friends

I'm intended to prove the following formula: subset?(g,v) where g={closed},
v={closed,open}.  I failed. The code is :

valve: type = {closed,open}
va: type=setof[valve]
v: var va                               % Do these statements correctly define v={closed, open} ?

guan: type = {i:valve |  i=closed}
gu: type =setof[guan]
g: var gu                               % Do these statements correctly define g={closed} ?

try: formula subset?(g,v)

The possible reasons might be sth relating to 'va: type=setof[valve]'. I'm very
confused by the precise meaning of variables defined by 'setof[T]'. For instance, 'va:
type=setof[valve]'. Since 'v: var va ', so, what's the value of 'v'? v={closed,open} or {open} or {closed} or {closed, open, {closed,open}} or all of these are possible? How to define a set like
v={closed, open} which contains 2 elements, one is 'closed', the other is 'open'.

I've checked the manuals, but didn't find the answers. Could anybody help me with the 2 questions? Thank you very much.

Pu