val u : type [infinite].
val a_u : type [approx_of u].
val up : a_u -> u [upcast].

val mem : u -> u -> prop.

# empty set
val emptySet : u.
axiom forall x. ~(mem x emptySet).

goal exists (x:u) (y:u). mem x y.