[BUG] Unsound skolemization when using \E as a value

[konnov]

The following test produces a spurious counterexample:

------------------------ MODULE ExistsAsValue -------------------------         
VARIABLES x

Init ==
    x = TRUE

Next ==
    x' = \E y \in {1, 2}: y /= 1

Next2 ==
    IF \E y \in {1, 2}: y /= 1
    THEN x' = TRUE
    ELSE x' = FALSE

Inv == x
=======================================================

The reason is that y is skolemized, though it is used as a value and thus effectively used both in negative and positive forms. The solution with Next2 disables the Skolemization of y and produces no counterexample. If an existential is used as a value, we should not skolemize it.

[konnov]

Fixed, SkolemizationMarker does not descend in the non-formula expressions any longer