cv_trans fails with "non-cv constant" on MEM with constructor list

(Generated with Claude Code)

When using cv_trans on a definition containing MEM x [Constructor1; Constructor2; ...], the translation fails with:

Exception: Encountered non-cv constant: Mod

Minimal example:

Given a datatype with constructors and a definition like:

```
Definition supported_arith_def[simp]:
(supported_arith a IntT =
if MEM a [Add; Sub; Mul; Div; Mod] then SOME (2:num) else NONE) ∧
(supported_arith a Float64T =
if MEM a [Abs; Neg; Sqrt] then SOME 1 else
if MEM a [Add; Sub; Mul; Div] then SOME 2 else
if a = FMA then SOME 3 else NONE) ∧
(supported_arith _ _ = NONE)
End
```

Running:
cv_trans supported_arith_def

Fails with the error about Mod (or whichever constructor appears in the list).

Workaround:

Applying SRULE [] before cv_trans works around the issue by simplifying the MEM expressions:
```
cv_trans (SRULE [] supported_arith_def)
```
Expected behavior:

cv_trans should either:
1. Automatically simplify MEM x [c1; c2; ...] into disjunctions (x = c1) ∨ (x = c2) ∨ ... before translation, or
2. Properly handle the MEM with a list of constructors

Context:

Encountered in CakeML regression testing (job 3089) when translating type inference code after adding new arithmetic operators.