# Next-state involving existential quantifier using PlusCal?

Hello,

I'm trying to specify a cache consistency protocol in PlusCal, and I'm having trouble with the step "the writer writes an arbitrary value to the database".

In TLA+, I would simply include the following conjunct:
• \E value \in Values \cup {Deleted} : db_value' = value
Is there a way to generate the same result in PlusCal?  I already tried the following:
• \E value \in Values \cup {Deleted} : db_value := value;
• This seems to generate \E' = [\E EXCEPT !value \in Values \cup {Deleted} : db_value = value]
• db_value := CHOOSE value \in Values \cup {Deleted} : TRUE;
• The semantics of using CHOOSE seems to be different than the semantics of using an existential quantifier
Thanks!
-Elliott