How to set a default for CHOOSE?

[wangq...@xxxxxxxxx]

I'm using CHOOSE, but it will catch error when no element is satisfied by p.

In my situation, I want to choose one element from a set or get a default element.

Like this:

```
some_set == {[key |-> 1, x |-> 1], [key |-> 2, x |-> 3], ...}

get_element(key) == 
  IF Cardinality({x \in some_set : x.key = key}) /= 0 
  THEN CHOOSE x \in some_set : x.key = key 
  ELSE [x |-> 0]

val == get_element(9).x
```

Is there a shorter way to represent `get_element`?