diff --git a/spectec/doc/Language.md b/spectec/doc/Language.md
index 376b54560a..cfe7438bc9 100644
--- a/spectec/doc/Language.md
+++ b/spectec/doc/Language.md
@@ -138,6 +138,7 @@ exp ::=
   exp "." atom                         record access
   exp "," exp                          record extension
   exp "++" exp                         list and record composition
+  exp "<-" exp                         list membership
   "|" exp "|"                          list length
   "||" gramid "||"                     expansion length
   "(" list(exp, ",") ")"               parentheses or tupling
diff --git a/spectec/spec/wasm-3.0/6-typing.watsup b/spectec/spec/wasm-3.0/6-typing.watsup
index e9364b1ef6..541cfc21b0 100644
--- a/spectec/spec/wasm-3.0/6-typing.watsup
+++ b/spectec/spec/wasm-3.0/6-typing.watsup
@@ -741,7 +741,7 @@ rule Instr_ok/ref.null:
 rule Instr_ok/ref.func:
   C |- REF.FUNC x : eps -> (REF dt)
   -- if C.FUNCS[x] = dt
-  -- if C.REFS = x_1* x x_2*  ;; TODO(2, rossberg): use elementof
+  -- if x <- C.REFS
 
 rule Instr_ok/ref.i31:
   C |- REF.I31 : I32 -> (REF I31)
@@ -1153,19 +1153,10 @@ rule Instr_const/global.get:
   C |- (GLOBAL.GET x) CONST
   -- if C.GLOBALS[x] = t
 
-;; TODO(2, rossberg): built in elemof
-def $in_numtype(numtype, numtype*) : bool    hint(show % <- %)
-def $in_numtype(nt, eps) = false
-def $in_numtype(nt, nt_1 nt'*) = nt = nt_1 \/ $in_numtype(nt, nt'*)
-
-def $in_binop(numtype, binop_(numtype), binop_(numtype)*) : bool  hint(show %2 <- %3)
-def $in_binop(nt, binop, eps) = false
-def $in_binop(nt, binop, (ibinop_1) ibinop'*) = binop = ibinop_1 \/ $in_binop(nt, binop, ibinop'*)
-
 rule Instr_const/binop:
   C |- (BINOP Inn binop) CONST
-  -- if $in_numtype(Inn, I32 I64)
-  -- if $in_binop(Inn, binop, ADD SUB MUL)
+  -- if Inn <- I32 I64
+  -- if binop <- ADD SUB MUL
 
 
 rule Expr_const: C |- instr* CONST
diff --git a/spectec/src/al/al_util.ml b/spectec/src/al/al_util.ml
index 5954be6830..f9a4776e71 100644
--- a/spectec/src/al/al_util.ml
+++ b/spectec/src/al/al_util.ml
@@ -47,6 +47,7 @@ let updE ?(at = no) (e1, pl, e2) = UpdE (e1, pl, e2) |> mk_expr at
 let extE ?(at = no) (e1, pl, e2, dir) = ExtE (e1, pl, e2, dir) |> mk_expr at
 let strE ?(at = no) r = StrE r |> mk_expr at
 let catE ?(at = no) (e1, e2) = CatE (e1, e2) |> mk_expr at
+let memE ?(at = no) (e1, e2) = MemE (e1, e2) |> mk_expr at
 let lenE ?(at = no) e = LenE e |> mk_expr at
 let tupE ?(at = no) el = TupE el |> mk_expr at
 let caseE ?(at = no) (a, el) = CaseE (a, el) |> mk_expr at
diff --git a/spectec/src/al/ast.ml b/spectec/src/al/ast.ml
index e80cc5f482..93fb299a69 100644
--- a/spectec/src/al/ast.ml
+++ b/spectec/src/al/ast.ml
@@ -85,6 +85,7 @@ and expr' =
   | ExtE of expr * path list * expr * extend_dir (* expr `[` path* `]` `:+` expr *)
   | StrE of (atom, expr) record         (* `{` (atom `->` expr)* `}` *)
   | CatE of expr * expr                 (* expr `++` expr *)
+  | MemE of expr * expr                 (* expr `<-` expr *)
   | LenE of expr                        (* `|` expr `|` *)
   | TupE of expr list                   (* `(` (expr `,`)* `)` *)
   | CaseE of atom * expr list           (* atom `(` expr* `)` -- MixE/CaseE *)
diff --git a/spectec/src/al/eq.ml b/spectec/src/al/eq.ml
index 3afb997502..8c05a5ba3b 100644
--- a/spectec/src/al/eq.ml
+++ b/spectec/src/al/eq.ml
@@ -30,6 +30,9 @@ let rec eq_expr e1 e2 =
   | CatE (e11, e12), CatE (e21, e22) ->
       eq_expr e11 e21 &&
       eq_expr e12 e22
+  | MemE (e11, e12), MemE (e21, e22) ->
+      eq_expr e11 e21 &&
+      eq_expr e12 e22
   | LenE e1, LenE e2 -> eq_expr e1 e2
   | TupE el1, TupE el2 -> eq_exprs el1 el2
   | CaseE (a1, el1), CaseE (a2, el2) ->
diff --git a/spectec/src/al/free.ml b/spectec/src/al/free.ml
index 09d38e90e5..78c95e22f6 100644
--- a/spectec/src/al/free.ml
+++ b/spectec/src/al/free.ml
@@ -28,6 +28,7 @@ let rec free_expr expr =
   | ContE e -> free_expr e
   | BinE (_, e1, e2)
   | CatE (e1, e2)
+  | MemE (e1, e2)
   | InfixE (e1, _, e2)
   | LabelE (e1, e2) -> free_expr e1 @ free_expr e2
   | FrameE (e_opt, e) -> free_opt free_expr e_opt @ free_expr e
diff --git a/spectec/src/al/print.ml b/spectec/src/al/print.ml
index 5624572997..77fe81258a 100644
--- a/spectec/src/al/print.ml
+++ b/spectec/src/al/print.ml
@@ -145,6 +145,8 @@ and string_of_expr expr =
   | CallE (id, el) -> sprintf "$%s(%s)" id (string_of_exprs ", " el)
   | CatE (e1, e2) ->
     sprintf "%s ++ %s" (string_of_expr e1) (string_of_expr e2)
+  | MemE (e1, e2) ->
+    sprintf "%s <- %s" (string_of_expr e1) (string_of_expr e2)
   | LenE e -> sprintf "|%s|" (string_of_expr e)
   | ArityE e -> sprintf "the arity of %s" (string_of_expr e)
   | GetCurStateE -> "the current state"
@@ -426,6 +428,12 @@ and structured_string_of_expr expr =
     ^ ", "
     ^ structured_string_of_expr e2
     ^ ")"
+  | MemE (e1, e2) ->
+    "MemE ("
+    ^ structured_string_of_expr e1
+    ^ ", "
+    ^ structured_string_of_expr e2
+    ^ ")"
   | LenE e -> "LenE (" ^ structured_string_of_expr e ^ ")"
   | ArityE e -> "ArityE (" ^ structured_string_of_expr e ^ ")"
   | GetCurStateE -> "GetCurStateE"
diff --git a/spectec/src/al/walk.ml b/spectec/src/al/walk.ml
index 1da2c87586..b5d85a9977 100644
--- a/spectec/src/al/walk.ml
+++ b/spectec/src/al/walk.ml
@@ -44,6 +44,7 @@ let rec walk_expr f e =
       (* TODO: Implement walker for iter *)
       | ListE el -> ListE (List.map new_ el)
       | CatE (e1, e2) -> CatE (new_ e1, new_ e2)
+      | MemE (e1, e2) -> MemE (new_ e1, new_ e2)
       | LenE e' -> LenE (new_ e')
       | StrE r -> StrE (Record.map id new_ r)
       | AccE (e, p) -> AccE (new_ e, walk_path f p)
diff --git a/spectec/src/backend-interpreter/interpreter.ml b/spectec/src/backend-interpreter/interpreter.ml
index 76a760fc3e..c0f8413ca1 100644
--- a/spectec/src/backend-interpreter/interpreter.ml
+++ b/spectec/src/backend-interpreter/interpreter.ml
@@ -150,6 +150,10 @@ and eval_expr env expr =
     | GeOp, v1, v2 -> boolV (v1 >= v2)
     | _ -> fail_expr expr "type mismatch for binary operation"
     )
+  (* Set Operation *)
+  | MemE (e1, e2) ->
+    let v1 = eval_expr env e1 in
+    eval_expr env e2 |> unwrap_listv_to_array |> Array.exists ((=) v1) |> boolV
   (* Function Call *)
   | CallE (fname, el) ->
     let args = List.map (eval_expr env) el in
diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml
index 7f6dfe68f8..c6e2348045 100644
--- a/spectec/src/backend-latex/render.ml
+++ b/spectec/src/backend-latex/render.ml
@@ -535,6 +535,10 @@ and expand_exp env ctxt e =
     let e1' = expand_exp env ctxt e1 in
     let e2' = expand_exp env ctxt e2 in
     CompE (e1', e2')
+  | MemE (e1, e2) ->
+    let e1' = expand_exp env ctxt e1 in
+    let e2' = expand_exp env ctxt e2 in
+    MemE (e1', e2')
   | LenE e1 ->
     let e1' = expand_exp env ctxt e1 in
     LenE e1'
@@ -1052,6 +1056,7 @@ Printf.eprintf "[render %s:X @ %s] try expansion\n%!" (Source.string_of_region e
   | DotE (e1, atom) -> render_exp env e1 ^ "{.}" ^ render_fieldname env atom
   | CommaE (e1, e2) -> render_exp env e1 ^ ", " ^ render_exp env e2
   | CompE (e1, e2) -> render_exp env e1 ^ " \\oplus " ^ render_exp env e2
+  | MemE (e1, e2) -> render_exp env e1 ^ " \\in " ^ render_exp env e2
   | LenE e1 -> "{|" ^ render_exp env e1 ^ "|}"
   | SizeE id -> "||" ^ render_gramid env id ^ "||"
   | ParenE ({it = SeqE [{it = AtomE atom; _}; _]; _} as e1, _)
diff --git a/spectec/src/backend-prose/gen.ml b/spectec/src/backend-prose/gen.ml
index e1bb615f89..400ae4f90b 100644
--- a/spectec/src/backend-prose/gen.ml
+++ b/spectec/src/backend-prose/gen.ml
@@ -56,6 +56,8 @@ let rec if_expr_to_instrs e =
       | _ -> print_yet_exp e "if_expr_to_instrs"; YetI (Il.Print.string_of_exp e) ]
   | Ast.BinE (Ast.EquivOp, e1, e2) ->
       [ EquivI (exp_to_expr e1, exp_to_expr e2) ]
+  | Ast.MemE (e1, e2) ->
+      [ MemI (exp_to_expr e1, exp_to_expr e2) ]
   | _ -> print_yet_exp e "if_expr_to_instrs"; [ YetI (Il.Print.string_of_exp e) ]
 
 let rec prem_to_instrs prem = match prem.it with
diff --git a/spectec/src/backend-prose/print.ml b/spectec/src/backend-prose/print.ml
index 482a2f02a9..5e91f8f52f 100644
--- a/spectec/src/backend-prose/print.ml
+++ b/spectec/src/backend-prose/print.ml
@@ -41,6 +41,10 @@ let rec string_of_instr = function
         (string_of_expr e1)
         (string_of_cmpop cmpop)
         (string_of_expr e2)
+  | MemI (e1, e2) ->
+      sprintf "%s %s must be contained in %s." (indent ())
+        (string_of_expr e1)
+        (string_of_expr e2)
   | MustValidI (e1, e2, eo) ->
       sprintf "%s Under the context %s, %s must be valid%s." (indent ())
         (string_of_expr e1)
diff --git a/spectec/src/backend-prose/prose.ml b/spectec/src/backend-prose/prose.ml
index f6a996d537..abfe19ee78 100644
--- a/spectec/src/backend-prose/prose.ml
+++ b/spectec/src/backend-prose/prose.ml
@@ -7,6 +7,7 @@ type cmpop = Eq | Ne | Lt | Gt | Le | Ge
 type instr =
 | LetI of Al.Ast.expr * Al.Ast.expr
 | CmpI of Al.Ast.expr * cmpop * Al.Ast.expr
+| MemI of Al.Ast.expr * Al.Ast.expr
 | MustValidI of Al.Ast.expr * Al.Ast.expr * Al.Ast.expr option
 | MustMatchI of Al.Ast.expr * Al.Ast.expr
 | IsValidI of Al.Ast.expr option
diff --git a/spectec/src/backend-prose/render.ml b/spectec/src/backend-prose/render.ml
index a3d0696454..4f43c9ddf0 100644
--- a/spectec/src/backend-prose/render.ml
+++ b/spectec/src/backend-prose/render.ml
@@ -417,6 +417,10 @@ let rec render_prose_instr env depth = function
       (String.capitalize_ascii (render_expr env e1))
       (render_prose_cmpop cmpop)
       (render_expr env e2)
+  | MemI (e1, e2) ->
+    sprintf "* %s must be contained in %s."
+      (String.capitalize_ascii (render_expr env e1))
+      (render_expr env e2)
   | MustValidI (e1, e2, e3) ->
     sprintf "* Under the context %s, %s must be valid%s."
       (render_expr env e1)
diff --git a/spectec/src/el/ast.ml b/spectec/src/el/ast.ml
index 900c2e3c63..832fc44eb9 100644
--- a/spectec/src/el/ast.ml
+++ b/spectec/src/el/ast.ml
@@ -117,6 +117,7 @@ and exp' =
   | DotE of exp * atom           (* exp `.` atom *)
   | CommaE of exp * exp          (* exp `,` exp *)
   | CompE of exp * exp           (* exp `++` exp *)
+  | MemE of exp * exp            (* exp `<-` exp *)
   | LenE of exp                  (* `|` exp `|` *)
   | SizeE of id                  (* `||` exp `||` *)
   | ParenE of exp * [`Sig | `Insig]  (* `(` exp `)` *)
diff --git a/spectec/src/el/atom.ml b/spectec/src/el/atom.ml
index c423aa82bf..3119ee264a 100644
--- a/spectec/src/el/atom.ml
+++ b/spectec/src/el/atom.ml
@@ -15,7 +15,7 @@ and atom' =
   | Dot3                         (* `...` *)
   | Semicolon                    (* `;` *)
   | Backslash                    (* `\` *)
-  | In                           (* `<-` *)
+  | Mem                          (* `<-` *)
   | Arrow                        (* `->` *)
   | Arrow2                       (* ``=>` *)
   | ArrowSub                     (* `->_` *)
@@ -71,7 +71,7 @@ let to_string atom =
   | Dot3 -> "..."
   | Semicolon -> ";"
   | Backslash -> "\\"
-  | In -> "in"
+  | Mem -> "<-"
   | Arrow -> "->"
   | Arrow2 -> "=>"
   | ArrowSub -> "->_"
@@ -120,7 +120,7 @@ let name atom =
   | Dot3 -> "dots"                (* Latex: \ldots *)
   | Semicolon -> "semicolon"      (* Latex: ; *)
   | Backslash -> "setminus"
-  | In -> "in"
+  | Mem -> "in"
   | Arrow -> "arrow"              (* Latex: \rightarrow *)
   | Arrow2 -> "darrow"            (* Latex: \Rightarrow *)
   | ArrowSub -> "arrowsub"        (* Latex: \rightarrow with subscript *)
diff --git a/spectec/src/el/eq.ml b/spectec/src/el/eq.ml
index aeb6a6ebc7..ea2ec8dfee 100644
--- a/spectec/src/el/eq.ml
+++ b/spectec/src/el/eq.ml
@@ -91,6 +91,7 @@ and eq_exp e1 e2 =
   | IdxE (e11, e12), IdxE (e21, e22)
   | CommaE (e11, e12), CommaE (e21, e22)
   | CompE (e11, e12), CompE (e21, e22)
+  | MemE (e11, e12), MemE (e21, e22)
   | FuseE (e11, e12), FuseE (e21, e22) -> eq_exp e11 e21 && eq_exp e12 e22
   | SliceE (e11, e12, e13), SliceE (e21, e22, e23) ->
     eq_exp e11 e21 && eq_exp e12 e22 && eq_exp e13 e23
diff --git a/spectec/src/el/free.ml b/spectec/src/el/free.ml
index aea56bde91..a4c9306a4b 100644
--- a/spectec/src/el/free.ml
+++ b/spectec/src/el/free.ml
@@ -130,7 +130,7 @@ and free_exp e =
   | ParenE (e1, _) | BrackE (_, e1, _) | ArithE e1 | UnparenE e1 -> free_exp e1
   | SizeE id -> free_gramid id
   | BinE (e1, _, e2) | CmpE (e1, _, e2)
-  | IdxE (e1, e2) | CommaE (e1, e2) | CompE (e1, e2)
+  | IdxE (e1, e2) | CommaE (e1, e2) | CompE (e1, e2) | MemE (e1, e2)
   | InfixE (e1, _, e2) | FuseE (e1, e2) -> free_exp e1 + free_exp e2
   | SliceE (e1, e2, e3) -> free_exp e1 + free_exp e2 + free_exp e3
   | SeqE es | TupE es -> free_list free_exp es
@@ -172,7 +172,7 @@ and det_exp e =
   | TypE (e1, _) -> det_exp e1
   | AtomE _ | BoolE _ | NatE _ | TextE _ | EpsE -> empty
   | UnE _ | BinE _ | CmpE _
-  | IdxE _ | SliceE _ | UpdE _ | ExtE _ | CommaE _ | CompE _
+  | IdxE _ | SliceE _ | UpdE _ | ExtE _ | CommaE _ | CompE _ | MemE _
   | DotE _ | LenE _ | SizeE _ -> idx_exp e
   | HoleE _ | FuseE _ | UnparenE _ | LatexE _ -> assert false
 
diff --git a/spectec/src/el/iter.ml b/spectec/src/el/iter.ml
index a5f5b81243..66c030be99 100644
--- a/spectec/src/el/iter.ml
+++ b/spectec/src/el/iter.ml
@@ -131,7 +131,7 @@ and exp e =
   | SizeE x -> gramid x
   | BinE (e1, op, e2) -> exp e1; binop op; exp e2
   | CmpE (e1, op, e2) -> exp e1; cmpop op; exp e2
-  | IdxE (e1, e2) | CommaE (e1, e2) | CompE (e1, e2)
+  | IdxE (e1, e2) | CommaE (e1, e2) | CompE (e1, e2) | MemE (e1, e2)
   | FuseE (e1, e2) -> exp e1; exp e2
   | SliceE (e1, e2, e3) -> exp e1; exp e2; exp e3
   | SeqE es | TupE es -> list exp es
@@ -282,6 +282,7 @@ and clone_exp e =
   | DotE (e1, atom) -> DotE (clone_exp e1, clone_atom atom)
   | CommaE (e1, e2) -> CommaE (clone_exp e1, clone_exp e2)
   | CompE (e1, e2) -> CompE (clone_exp e1, clone_exp e2)
+  | MemE (e1, e2) -> MemE (clone_exp e1, clone_exp e2)
   | LenE e1 -> LenE (clone_exp e1)
   | ParenE (e1, b) -> ParenE (clone_exp e1, b)
   | TupE es -> TupE (List.map clone_exp es)
diff --git a/spectec/src/el/print.ml b/spectec/src/el/print.ml
index db16f0ef86..0000c87598 100644
--- a/spectec/src/el/print.ml
+++ b/spectec/src/el/print.ml
@@ -155,6 +155,7 @@ and string_of_exp e =
   | DotE (e1, atom) -> string_of_exp e1 ^ "." ^ string_of_atom atom
   | CommaE (e1, e2) -> string_of_exp e1 ^ ", " ^ string_of_exp e2
   | CompE (e1, e2) -> string_of_exp e1 ^ " ++ " ^ string_of_exp e2
+  | MemE (e1, e2) -> string_of_exp e1 ^ " <- " ^ string_of_exp e2
   | LenE e1 -> "|" ^ string_of_exp e1 ^ "|"
   | SizeE id -> "||" ^ string_of_gramid id ^ "||"
   | ParenE (e, signif) ->
diff --git a/spectec/src/el/subst.ml b/spectec/src/el/subst.ml
index 37b05c3bd9..127b1caf66 100644
--- a/spectec/src/el/subst.ml
+++ b/spectec/src/el/subst.ml
@@ -138,6 +138,7 @@ and subst_exp s e =
   | DotE (e1, atom) -> DotE (subst_exp s e1, atom)
   | CommaE (e1, e2) -> CommaE (subst_exp s e1, subst_exp s e2)
   | CompE (e1, e2) -> CompE (subst_exp s e1, subst_exp s e2)
+  | MemE (e1, e2) -> MemE (subst_exp s e1, subst_exp s e2)
   | LenE e1 -> LenE (subst_exp s e1)
   | SizeE id -> SizeE (subst_gramid s id)
   | ParenE (e1, b) -> ParenE (subst_exp s e1, b)
diff --git a/spectec/src/frontend/dim.ml b/spectec/src/frontend/dim.ml
index 457e24943c..ca52b0a60e 100644
--- a/spectec/src/frontend/dim.ml
+++ b/spectec/src/frontend/dim.ml
@@ -145,6 +145,7 @@ and check_exp env ctx e =
   | IdxE (e1, e2)
   | CommaE (e1, e2)
   | CompE (e1, e2)
+  | MemE (e1, e2)
   | InfixE (e1, _, e2) ->
     check_exp env ctx e1;
     check_exp env ctx e2
@@ -404,6 +405,10 @@ and annot_exp env e : Il.Ast.exp * occur =
     | ListE es ->
       let es', occurs = List.split (List.map (annot_exp env) es) in
       ListE es', List.fold_left union Env.empty occurs
+    | MemE (e1, e2) ->
+      let e1', occur1 = annot_exp env e1 in
+      let e2', occur2 = annot_exp env e2 in
+      MemE (e1', e2'), union occur1 occur2
     | CatE (e1, e2) ->
       let e1', occur1 = annot_exp env e1 in
       let e2', occur2 = annot_exp env e2 in
diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml
index 805c62f2f1..fbacdc654e 100644
--- a/spectec/src/frontend/elab.ml
+++ b/spectec/src/frontend/elab.ml
@@ -985,6 +985,10 @@ and infer_exp' env e : Il.exp' * typ =
     let _ = as_comp_typ "expression" env Infer t1 e.at in
     let e2' = elab_exp env e2 t1 in
     Il.CompE (e1', e2'), t1
+  | MemE (e1, e2) ->
+    let e1', t1 = infer_exp env e1 in
+    let e2' = elab_exp env e2 (IterT (t1, List) $ e2.at) in
+    Il.MemE (e1', e2'), BoolT $ e.at
   | LenE e1 ->
     let e1', t1 = infer_exp env e1 in
     let _t11 = as_list_typ "expression" env Infer t1 e1.at in
@@ -1122,6 +1126,9 @@ and elab_exp' env e t : Il.exp' =
     let e1' = elab_exp env e1 t in
     let e2' = elab_exp env e2 t in
     Il.CompE (e1', e2')
+  | MemE _ ->
+    let e', t' = infer_exp env e in
+    cast_exp' "element operator" env e' t' t
   | LenE _ ->
     let e', t' = infer_exp env e in
     cast_exp' "list length" env e' t' t
diff --git a/spectec/src/frontend/eval.ml b/spectec/src/frontend/eval.ml
index 2192f26244..48cd322f24 100644
--- a/spectec/src/frontend/eval.ml
+++ b/spectec/src/frontend/eval.ml
@@ -282,6 +282,20 @@ and reduce_exp env e : exp =
       in StrE (merge efs1 efs2)
     | _ -> CompE (e1', e2')
     ) $ e.at
+  | MemE (e1, e2) ->
+    let e1' = reduce_exp env e1 in
+    let e2' = reduce_exp env e2 in
+    (match e2'.it with
+    | SeqE [] -> BoolE false $ e.at
+    | SeqE (e21'::es2') ->
+      reduce_exp env (BinE (
+        CmpE (e1', EqOp, e21') $ e.at,
+        OrOp,
+        MemE (e1', SeqE es2' $ e2.at) $ e.at
+      ) $ e.at)
+    | _ when is_normal_exp e2' -> reduce_exp env (CmpE (e1', EqOp, e2') $ e.at)
+    | _ -> MemE (e1', e2') $ e.at
+    )
   | LenE e1 ->
     let e1' = reduce_exp env e1 in
     (match e1'.it with
diff --git a/spectec/src/frontend/lexer.mll b/spectec/src/frontend/lexer.mll
index eef821d367..c92e93f1bf 100644
--- a/spectec/src/frontend/lexer.mll
+++ b/spectec/src/frontend/lexer.mll
@@ -184,7 +184,7 @@ and token = parse
   | "+-" { PLUSMINUS }
   | "-+" { MINUSPLUS }
 
-  | "<-" { IN }
+  | "<-" { MEM }
   | "->" { ARROW }
   | "=>" { ARROW2 }
   | "->_" { ARROWSUB }
diff --git a/spectec/src/frontend/parser.mly b/spectec/src/frontend/parser.mly
index f00c7cc992..aeece560ba 100644
--- a/spectec/src/frontend/parser.mly
+++ b/spectec/src/frontend/parser.mly
@@ -69,7 +69,7 @@ let rec prec_of_exp = function  (* as far as iteration is concerned *)
   | ParenE _ | TupE _ | BrackE _ | CallE _ | HoleE _ -> Prim
   | AtomE _ | IdxE _ | SliceE _ | UpdE _ | ExtE _ | DotE _ | IterE _ -> Post
   | SeqE _ -> Seq
-  | UnE _ | BinE _ | CmpE _ | InfixE _ | LenE _ | SizeE _
+  | UnE _ | BinE _ | CmpE _ | MemE _ | InfixE _ | LenE _ | SizeE _
   | CommaE _ | CompE _ | TypE _ | FuseE _ | UnparenE _ | LatexE _ -> Op
   | ArithE e -> prec_of_exp e.it
 
@@ -123,7 +123,7 @@ let rec is_typcon t =
 %token NOT AND OR
 %token QUEST PLUS MINUS STAR SLASH BACKSLASH UP COMPOSE PLUSMINUS MINUSPLUS
 %token ARROW ARROW2 ARROWSUB ARROW2SUB DARROW2 SQARROW SQARROWSTAR
-%token IN PREC SUCC TURNSTILE TILESTURN
+%token MEM PREC SUCC TURNSTILE TILESTURN
 %token DOLLAR TICK
 %token BOT TOP
 %token HOLE MULTIHOLE NOTHING FUSE FUSEFUSE LATEX
@@ -146,7 +146,7 @@ let rec is_typcon t =
 %right SQARROW SQARROWSTAR PREC SUCC BIGCOMP BIGAND BIGOR
 %left COLON SUB SUP ASSIGN EQUIV APPROX
 %left COMMA COMMA_NL
-%right EQ NE LT GT LE GE IN
+%right EQ NE LT GT LE GE MEM
 %right ARROW ARROWSUB
 %left SEMICOLON
 %left DOT DOTDOT DOTDOTDOT
@@ -252,6 +252,7 @@ atom_ :
   | atom_escape { $1 }
 atom_escape :
   | TICK EQ { Atom.Equal }
+  | TICK MEM { Atom.Mem }
   | TICK QUEST { Atom.Quest }
   | TICK PLUS { Atom.Plus }
   | TICK STAR { Atom.Star }
@@ -343,7 +344,6 @@ check_atom :
   | SUCC { Atom.Succ }
   | TILESTURN { Atom.Tilesturn }
   | TURNSTILE { Atom.Turnstile }
-  | IN { Atom.In }
 
 
 (* Iteration *)
@@ -583,6 +583,7 @@ exp_bin_ :
   | exp_bin COMPOSE exp_bin { CompE ($1, $3) }
   | exp_bin infixop exp_bin { InfixE ($1, $2, $3) }
   | exp_bin cmpop exp_bin { CmpE ($1, $2, $3) }
+  | exp_bin MEM exp_bin { MemE ($1, $3) }
   | exp_bin boolop exp_bin { BinE ($1, $2, $3) }
 
 exp_rel : exp_rel_ { $1 $ $sloc }
@@ -647,6 +648,7 @@ arith_bin_ :
   | arith_un_ { $1 }
   | arith_bin binop arith_bin { BinE ($1, $2, $3) }
   | arith_bin cmpop arith_bin { CmpE ($1, $2, $3) }
+  | arith_bin MEM arith_bin { MemE ($1, $3) }
   | arith_bin boolop arith_bin { BinE ($1, $2, $3) }
 
 arith : arith_bin { $1 }
diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml
index 0d7298956c..84702d0a54 100644
--- a/spectec/src/il/ast.ml
+++ b/spectec/src/il/ast.ml
@@ -94,6 +94,7 @@ and exp' =
   | DotE of exp * atom           (* exp.atom *)
   | CompE of exp * exp           (* exp @ exp *)
   | ListE of exp list            (* [exp ... exp] *)
+  | MemE of exp * exp            (* exp `<-` exp *)
   | LenE of exp                  (* |exp| *)
   | CatE of exp * exp            (* exp :: exp *)
   | IdxE of exp * exp            (* exp[exp]` *)
diff --git a/spectec/src/il/eq.ml b/spectec/src/il/eq.ml
index 9b06f15699..d19a51732e 100644
--- a/spectec/src/il/eq.ml
+++ b/spectec/src/il/eq.ml
@@ -75,6 +75,7 @@ and eq_exp e1 e2 =
   | LenE e11, LenE e21 -> eq_exp e11 e21
   | IdxE (e11, e12), IdxE (e21, e22)
   | CompE (e11, e12), CompE (e21, e22)
+  | MemE (e11, e12), MemE (e21, e22)
   | CatE (e11, e12), CatE (e21, e22) -> eq_exp e11 e21 && eq_exp e12 e22
   | SliceE (e11, e12, e13), SliceE (e21, e22, e23) ->
     eq_exp e11 e21 && eq_exp e12 e22 && eq_exp e13 e23
diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml
index 3110294fa0..8f181d9f68 100644
--- a/spectec/src/il/eval.ml
+++ b/spectec/src/il/eval.ml
@@ -245,6 +245,19 @@ and reduce_exp env e : exp =
       in StrE (List.map2 merge efs1 efs2)
     | _ -> CompE (e1', e2')
     ) $> e
+  | MemE (e1, e2) ->
+    let e1' = reduce_exp env e1 in
+    let e2' = reduce_exp env e2 in
+    (match e2'.it with
+    | OptE None | ListE [] -> BoolE false $> e
+    | OptE (Some e21') -> reduce_exp env (CmpE (EqOp, e1', e21') $> e)
+    | ListE (e21'::es2') ->
+      reduce_exp env (BinE (OrOp,
+        CmpE (EqOp, e1', e21') $> e,
+        MemE (e1', ListE es2' $> e2) $> e
+      ) $> e)
+    | _ -> MemE (e1', e2') $> e
+    )
   | LenE e1 ->
     let e1' = reduce_exp env e1 in
     (match e1'.it with
diff --git a/spectec/src/il/free.ml b/spectec/src/il/free.ml
index 6a186ef478..50352a08e1 100644
--- a/spectec/src/il/free.ml
+++ b/spectec/src/il/free.ml
@@ -109,7 +109,7 @@ and free_exp e =
   | BoolE _ | NatE _ | TextE _ -> empty
   | UnE (_, e1) | LenE e1 | ProjE (e1, _) | TheE e1 | DotE (e1, _) -> free_exp e1
   | BinE (_, e1, e2) | CmpE (_, e1, e2)
-  | IdxE (e1, e2) | CompE (e1, e2) | CatE (e1, e2) -> free_exp e1 + free_exp e2
+  | IdxE (e1, e2) | CompE (e1, e2) | MemE (e1, e2) | CatE (e1, e2) -> free_exp e1 + free_exp e2
   | SliceE (e1, e2, e3) -> free_list free_exp [e1; e2; e3]
   | OptE eo -> free_opt free_exp eo
   | TupE es | ListE es -> free_list free_exp es
diff --git a/spectec/src/il/iter.ml b/spectec/src/il/iter.ml
index cc88b7f4cf..599a40c031 100644
--- a/spectec/src/il/iter.ml
+++ b/spectec/src/il/iter.ml
@@ -127,7 +127,7 @@ and exp e =
   | OptE eo -> opt exp eo
   | StrE efs -> list expfield efs
   | DotE (e1, at) -> exp e1; atom at
-  | CompE (e1, e2) | CatE (e1, e2) | IdxE (e1, e2) -> exp e1; exp e2
+  | CompE (e1, e2) | MemE (e1, e2) | CatE (e1, e2) | IdxE (e1, e2) -> exp e1; exp e2
   | SliceE (e1, e2, e3) -> exp e1; exp e2; exp e3
   | UpdE (e1, p, e2) | ExtE (e1, p, e2) -> exp e1; path p; exp e2
   | CallE (x, as_) -> defid x; args as_
diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml
index 213c51ec70..15204bded5 100644
--- a/spectec/src/il/print.ml
+++ b/spectec/src/il/print.ml
@@ -134,6 +134,7 @@ and string_of_exp e =
   | DotE (e1, atom) ->
     string_of_exp e1 ^ "." ^ string_of_mixop [[atom]] ^ "_" ^ string_of_typ_name e1.note
   | CompE (e1, e2) -> string_of_exp e1 ^ " ++ " ^ string_of_exp e2
+  | MemE (e1, e2) -> string_of_exp e1 ^ " <- " ^ string_of_exp e2
   | LenE e1 -> "|" ^ string_of_exp e1 ^ "|"
   | TupE es -> "(" ^ string_of_exps ", " es ^ ")"
   | CallE (id, as1) -> "$" ^ id.it ^ string_of_args as1
diff --git a/spectec/src/il/subst.ml b/spectec/src/il/subst.ml
index a130cbe23b..b2dc52be9e 100644
--- a/spectec/src/il/subst.ml
+++ b/spectec/src/il/subst.ml
@@ -118,6 +118,7 @@ and subst_exp s e =
   | StrE efs -> StrE (subst_list subst_expfield s efs)
   | DotE (e1, atom) -> DotE (subst_exp s e1, atom)
   | CompE (e1, e2) -> CompE (subst_exp s e1, subst_exp s e2)
+  | MemE (e1, e2) -> MemE (subst_exp s e1, subst_exp s e2)
   | LenE e1 -> LenE (subst_exp s e1)
   | TupE es -> TupE (subst_list subst_exp s es)
   | CallE (id, as_) -> CallE (subst_defid s id, subst_args s as_)
diff --git a/spectec/src/il/valid.ml b/spectec/src/il/valid.ml
index 1bb67fcb98..a4eab1250f 100644
--- a/spectec/src/il/valid.ml
+++ b/spectec/src/il/valid.ml
@@ -287,7 +287,7 @@ and infer_exp env e : typ =
   | TextE _ -> TextT $ e.at
   | UnE (op, _) -> let _t1, t' = infer_unop op in t' $ e.at
   | BinE (op, _, _) -> let _t1, _t2, t' = infer_binop op in t' $ e.at
-  | CmpE _ -> BoolT $ e.at
+  | CmpE _ | MemE _ -> BoolT $ e.at
   | IdxE (e1, _) -> as_list_typ "expression" env Infer (infer_exp env e1) e1.at
   | SliceE (e1, _, _)
   | UpdE (e1, _, _)
@@ -400,6 +400,11 @@ try
     let _ = as_comp_typ "expression" env Check t e.at in
     valid_exp env e1 t;
     valid_exp env e2 t
+  | MemE (e1, e2) ->
+    let t1 = infer_exp env e1 in
+    valid_exp env e1 t1;
+    valid_exp env e2 (IterT (t1, List) $ e2.at);
+    equiv_typ env (BoolT $ e.at) t e.at
   | LenE e1 ->
     let t1 = infer_exp env e1 in
     let _typ11 = as_list_typ "expression" env Infer t1 e1.at in
diff --git a/spectec/src/il2al/free.ml b/spectec/src/il2al/free.ml
index 157026e9e5..8c35b99bcf 100644
--- a/spectec/src/il2al/free.ml
+++ b/spectec/src/il2al/free.ml
@@ -25,7 +25,7 @@ let rec free_exp ignore_listN e =
   | UnE (_, e1) | LenE e1 | TheE e1 | SubE (e1, _, _)
   | DotE (e1, _) | CaseE (_, e1) | ProjE (e1, _) | UncaseE (e1, _) ->
     f e1
-  | BinE (_, e1, e2) | CmpE (_, e1, e2) | IdxE (e1, e2) | CompE (e1, e2) | CatE (e1, e2) ->
+  | BinE (_, e1, e2) | CmpE (_, e1, e2) | IdxE (e1, e2) | CompE (e1, e2) | MemE (e1, e2) | CatE (e1, e2) ->
     free_list f [e1; e2]
   | SliceE (e1, e2, e3) -> free_list f [e1; e2; e3]
   | OptE eo -> free_opt f eo
diff --git a/spectec/src/il2al/il2il.ml b/spectec/src/il2al/il2il.ml
index 996c085cb8..cea17e95c2 100644
--- a/spectec/src/il2al/il2il.ml
+++ b/spectec/src/il2al/il2il.ml
@@ -47,6 +47,7 @@ let rec transform_expr f e =
     | TheE e1 -> TheE (new_ e1)
     | ListE es -> ListE ((List.map new_) es)
     | CatE (e1, e2) -> CatE (new_ e1, new_ e2)
+    | MemE (e1, e2) -> MemE (new_ e1, new_ e2)
     | CaseE (mixop, e1) -> CaseE (mixop, new_ e1)
     | SubE (e1, _t1, t2) -> SubE (new_ e1, _t1, t2)
   in { e with it }
@@ -161,6 +162,8 @@ let rec overlap e1 e2 = if eq_exp e1 e2 then e1 else
       ListE (List.map2 overlap es1 es2) |> replace_it
     | CatE (e1, e1'), CatE (e2, e2') ->
       CatE (overlap e1 e2, overlap e1' e2') |> replace_it
+    | MemE (e1, e1'), MemE (e2, e2') ->
+      MemE (overlap e1 e2, overlap e1' e2') |> replace_it
     | CaseE (mixop1, e1), CaseE (mixop2, e2) when eq_mixop mixop1 mixop2 ->
       CaseE (mixop1, overlap e1 e2) |> replace_it
     | SubE (e1, typ1, typ1'), SubE (e2, typ2, typ2') when eq_typ typ1 typ2 && eq_typ typ1' typ2' ->
@@ -223,6 +226,7 @@ let rec collect_unified template e = if eq_exp template e then [], [] else
     | ExtE (e1, _, e1'), ExtE (e2, _, e2')
     | CompE (e1, e1'), CompE (e2, e2')
     | CatE (e1, e1'), CatE (e2, e2') -> pairwise_concat (collect_unified e1 e2) (collect_unified e1' e2')
+    | MemE (e1, e1'), MemE (e2, e2') -> pairwise_concat (collect_unified e1 e2) (collect_unified e1' e2')
     | SliceE (e1, e1', e1''), SliceE (e2, e2', e2'') ->
       pairwise_concat (pairwise_concat (collect_unified e1 e2) (collect_unified e1' e2')) (collect_unified e1'' e2'')
     | StrE efs1, StrE efs2 ->
diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml
index bdb8ba82cb..e18588bf13 100644
--- a/spectec/src/il2al/translate.ml
+++ b/spectec/src/il2al/translate.ml
@@ -200,6 +200,11 @@ and translate_exp exp =
       | Il.GeOp _ -> GeOp
     in
     binE (compare_op, lhs, rhs) ~at:at
+  (* Set operation *)
+  | Il.MemE (exp1, exp2) ->
+    let lhs = translate_exp exp1 in
+    let rhs = translate_exp exp2 in
+    memE (lhs, rhs) ~at:at
   (* Tuple *)
   | Il.TupE [e] -> translate_exp e
   | Il.TupE exps -> tupE (List.map translate_exp exps) ~at:at
diff --git a/spectec/src/middlend/sideconditions.ml b/spectec/src/middlend/sideconditions.ml
index 354f501d89..3b0e8c0171 100644
--- a/spectec/src/middlend/sideconditions.ml
+++ b/spectec/src/middlend/sideconditions.ml
@@ -88,6 +88,7 @@ let rec t_exp env e : prem list =
   | CmpE (_, exp1, exp2)
   | IdxE (exp1, exp2)
   | CompE (exp1, exp2)
+  | MemE (exp1, exp2)
   | CatE (exp1, exp2)
   -> t_exp env exp1 @ t_exp env exp2
   | SliceE (exp1, exp2, exp3)
diff --git a/spectec/src/middlend/sub.ml b/spectec/src/middlend/sub.ml
index b05cd8c85c..46e39e9e43 100644
--- a/spectec/src/middlend/sub.ml
+++ b/spectec/src/middlend/sub.ml
@@ -161,6 +161,7 @@ and t_exp' env = function
   | TheE exp -> TheE exp
   | ListE es -> ListE (List.map (t_exp env) es)
   | CatE (exp1, exp2) -> CatE (t_exp env exp1, t_exp env exp2)
+  | MemE (exp1, exp2) -> MemE (t_exp env exp1, t_exp env exp2)
   | CaseE (mixop, e) -> CaseE (mixop, t_exp env e)
   | SubE (e, t1, t2) -> SubE (e, t1, t2)
 
diff --git a/spectec/src/middlend/totalize.ml b/spectec/src/middlend/totalize.ml
index c11f6bf20e..4feca23ed1 100644
--- a/spectec/src/middlend/totalize.ml
+++ b/spectec/src/middlend/totalize.ml
@@ -100,6 +100,7 @@ and t_exp' env = function
   | TheE exp -> TheE exp
   | ListE es -> ListE (List.map (t_exp env) es)
   | CatE (exp1, exp2) -> CatE (t_exp env exp1, t_exp env exp2)
+  | MemE (exp1, exp2) -> MemE (t_exp env exp1, t_exp env exp2)
   | CaseE (mixop, e) -> CaseE (mixop, t_exp env e)
   | SubE (exp, t1, t2) -> SubE (t_exp env exp, t_typ env t1, t_typ env t2)
 
diff --git a/spectec/src/middlend/unthe.ml b/spectec/src/middlend/unthe.ml
index 6aa615c122..a9cbe938f0 100644
--- a/spectec/src/middlend/unthe.ml
+++ b/spectec/src/middlend/unthe.ml
@@ -136,6 +136,7 @@ and t_exp' n e : eqns * exp' =
   | IdxE (exp1, exp2) -> t_ee n (exp1, exp2) (fun (e1', e2') -> IdxE (e1', e2'))
   | CompE (exp1, exp2) -> t_ee n (exp1, exp2) (fun (e1', e2') -> CompE (e1', e2'))
   | CatE (exp1, exp2) -> t_ee n (exp1, exp2) (fun (e1', e2') -> CatE (e1', e2'))
+  | MemE (exp1, exp2) -> t_ee n (exp1, exp2) (fun (e1', e2') -> MemE (e1', e2'))
 
   | SliceE (exp1, exp2, exp3) -> t_eee n (exp1, exp2, exp3) (fun (e1', e2', e3') -> SliceE (e1', e2', e3'))
 
diff --git a/spectec/src/middlend/wild.ml b/spectec/src/middlend/wild.ml
index 870664de79..ccf738baee 100644
--- a/spectec/src/middlend/wild.ml
+++ b/spectec/src/middlend/wild.ml
@@ -158,6 +158,7 @@ and t_exp' env e : bind list * exp' =
   | IdxE (exp1, exp2) -> t_ee env (exp1, exp2) (fun (e1', e2') -> IdxE (e1', e2'))
   | CompE (exp1, exp2) -> t_ee env (exp1, exp2) (fun (e1', e2') -> CompE (e1', e2'))
   | CatE (exp1, exp2) -> t_ee env (exp1, exp2) (fun (e1', e2') -> CatE (e1', e2'))
+  | MemE (exp1, exp2) -> t_ee env (exp1, exp2) (fun (e1', e2') -> MemE (e1', e2'))
 
   | SliceE (exp1, exp2, exp3) -> t_eee env (exp1, exp2, exp3) (fun (e1', e2', e3') -> SliceE (e1', e2', e3'))
 
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index 9ff19aac93..5fac054b93 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -4220,11 +4220,11 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
     `%|-%:%`(C, REF.NULL_instr(ht), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(`NULL%?`_nul(?(())), ht)])))
     -- Heaptype_ok: `%|-%:OK`(C, ht)
 
-  ;; 6-typing.watsup:741.1-744.29
-  rule ref.func{C : context, x : idx, dt : deftype, x_1* : idx*, x_2* : idx*}:
+  ;; 6-typing.watsup:741.1-744.20
+  rule ref.func{C : context, x : idx, dt : deftype}:
     `%|-%:%`(C, REF.FUNC_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(`NULL%?`_nul(?()), (dt : deftype <: heaptype))])))
     -- if (C.FUNCS_context[x!`%`_idx.0] = dt)
-    -- if (C.REFS_context = x_1*{x_1 : funcidx} :: [x] :: x_2*{x_2 : funcidx})
+    -- if x <- C.REFS_context
 
   ;; 6-typing.watsup:746.1-747.34
   rule ref.i31{C : context}:
@@ -4650,28 +4650,6 @@ relation Expr_ok: `%|-%:%`(context, expr, resulttype)
     `%|-%:%`(C, instr*{instr : instr}, `%`_resulttype(t*{t : valtype}))
     -- Instrs_ok: `%|-%:%`(C, instr*{instr : instr}, `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype(t*{t : valtype})))
 
-;; 6-typing.watsup
-rec {
-
-;; 6-typing.watsup:1161.1-1161.86
-def $in_binop(numtype : numtype, binop_ : binop_(numtype), binop_(numtype)*) : bool
-  ;; 6-typing.watsup:1162.1-1162.38
-  def $in_binop{nt : numtype, binop : binop_(nt)}(nt, binop, []) = false
-  ;; 6-typing.watsup:1163.1-1163.99
-  def $in_binop{nt : numtype, binop : binop_(nt), ibinop_1 : binop_(nt), ibinop'* : binop_(nt)*}(nt, binop, [ibinop_1] :: ibinop'*{ibinop' : binop_(nt)}) = ((binop = ibinop_1) \/ $in_binop(nt, binop, ibinop'*{ibinop' : binop_(nt)}))
-}
-
-;; 6-typing.watsup
-rec {
-
-;; 6-typing.watsup:1157.1-1157.63
-def $in_numtype(numtype : numtype, numtype*) : bool
-  ;; 6-typing.watsup:1158.1-1158.33
-  def $in_numtype{nt : numtype}(nt, []) = false
-  ;; 6-typing.watsup:1159.1-1159.68
-  def $in_numtype{nt : numtype, nt_1 : numtype, nt'* : numtype*}(nt, [nt_1] :: nt'*{nt' : numtype}) = ((nt = nt_1) \/ $in_numtype(nt, nt'*{nt' : numtype}))
-}
-
 ;; 6-typing.watsup
 relation Instr_const: `%|-%CONST`(context, instr)
   ;; 6-typing.watsup
@@ -4730,8 +4708,8 @@ relation Instr_const: `%|-%CONST`(context, instr)
   ;; 6-typing.watsup
   rule binop{C : context, Inn : Inn, binop : binop_((Inn : Inn <: numtype))}:
     `%|-%CONST`(C, BINOP_instr((Inn : Inn <: numtype), binop))
-    -- if $in_numtype((Inn : Inn <: numtype), [I32_numtype I64_numtype])
-    -- if $in_binop((Inn : Inn <: numtype), binop, [ADD_binop_ SUB_binop_ MUL_binop_])
+    -- if Inn <- [I32_Inn I64_Inn]
+    -- if binop <- [ADD_binop_ SUB_binop_ MUL_binop_]
 
 ;; 6-typing.watsup
 relation Expr_const: `%|-%CONST`(context, expr)
@@ -4894,13 +4872,13 @@ relation Export_ok: `%|-%:%`(context, export, externtype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1306.1-1306.100
+;; 6-typing.watsup:1297.1-1297.100
 relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
-  ;; 6-typing.watsup:1348.1-1349.17
+  ;; 6-typing.watsup:1339.1-1340.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1351.1-1354.55
+  ;; 6-typing.watsup:1342.1-1345.55
   rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}:
     `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype})
     -- Global_ok: `%|-%:%`(C, global, gt_1)
@@ -4910,13 +4888,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1305.1-1305.98
+;; 6-typing.watsup:1296.1-1296.98
 relation Types_ok: `%|-%:%`(context, type*, deftype*)
-  ;; 6-typing.watsup:1340.1-1341.17
+  ;; 6-typing.watsup:1331.1-1332.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1343.1-1346.50
+  ;; 6-typing.watsup:1334.1-1337.50
   rule cons{C : context, type_1 : type, type* : type*, dt_1* : deftype*, dt* : deftype*}:
     `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{dt_1 : deftype} :: dt*{dt : deftype})
     -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype})
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index 79e6094fc7..aa0d1667e9 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -5644,7 +5644,7 @@ $$
 \frac{
 C{.}\mathsf{funcs}{}[x] = {\mathit{dt}}
  \qquad
-C{.}\mathsf{refs} = {x_1^\ast}~x~{x_2^\ast}
+x \in C{.}\mathsf{refs}
 }{
 C \vdash \mathsf{ref{.}func}~x : \epsilon \rightarrow (\mathsf{ref}~{\mathit{dt}})
 } \, {[\textsc{\scriptsize T{-}ref.func}]}
@@ -6686,20 +6686,6 @@ C \vdash (\mathsf{global{.}get}~x)~\mathsf{const}
 \end{array}
 $$
 
-$$
-\begin{array}{@{}lcl@{}l@{}}
-{\mathit{nt}} \in \epsilon &=& \mathsf{false} \\
-{\mathit{nt}} \in {\mathit{nt}}_1~{{\mathit{nt}'}^\ast} &=& {\mathit{nt}} = {\mathit{nt}}_1 \lor {\mathit{nt}} \in {{\mathit{nt}'}^\ast} \\
-\end{array}
-$$
-
-$$
-\begin{array}{@{}lcl@{}l@{}}
-{\mathit{binop}} \in \epsilon &=& \mathsf{false} \\
-{\mathit{binop}} \in ({\mathit{ibinop}}_1)~{{\mathit{ibinop}'}^\ast} &=& {\mathit{binop}} = {\mathit{ibinop}}_1 \lor {\mathit{binop}} \in {{\mathit{ibinop}'}^\ast} \\
-\end{array}
-$$
-
 $$
 \begin{array}{@{}c@{}}\displaystyle
 \frac{
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
index a4a528c9b9..ed7c042582 100644
--- a/spectec/test-middlend/TEST.md
+++ b/spectec/test-middlend/TEST.md
@@ -4210,11 +4210,11 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
     `%|-%:%`(C, REF.NULL_instr(ht), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(`NULL%?`_nul(?(())), ht)])))
     -- Heaptype_ok: `%|-%:OK`(C, ht)
 
-  ;; 6-typing.watsup:741.1-744.29
-  rule ref.func{C : context, x : idx, dt : deftype, x_1* : idx*, x_2* : idx*}:
+  ;; 6-typing.watsup:741.1-744.20
+  rule ref.func{C : context, x : idx, dt : deftype}:
     `%|-%:%`(C, REF.FUNC_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(`NULL%?`_nul(?()), (dt : deftype <: heaptype))])))
     -- if (C.FUNCS_context[x!`%`_idx.0] = dt)
-    -- if (C.REFS_context = x_1*{x_1 : funcidx} :: [x] :: x_2*{x_2 : funcidx})
+    -- if x <- C.REFS_context
 
   ;; 6-typing.watsup:746.1-747.34
   rule ref.i31{C : context}:
@@ -4640,28 +4640,6 @@ relation Expr_ok: `%|-%:%`(context, expr, resulttype)
     `%|-%:%`(C, instr*{instr : instr}, `%`_resulttype(t*{t : valtype}))
     -- Instrs_ok: `%|-%:%`(C, instr*{instr : instr}, `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype(t*{t : valtype})))
 
-;; 6-typing.watsup
-rec {
-
-;; 6-typing.watsup:1161.1-1161.86
-def $in_binop(numtype : numtype, binop_ : binop_(numtype), binop_(numtype)*) : bool
-  ;; 6-typing.watsup:1162.1-1162.38
-  def $in_binop{nt : numtype, binop : binop_(nt)}(nt, binop, []) = false
-  ;; 6-typing.watsup:1163.1-1163.99
-  def $in_binop{nt : numtype, binop : binop_(nt), ibinop_1 : binop_(nt), ibinop'* : binop_(nt)*}(nt, binop, [ibinop_1] :: ibinop'*{ibinop' : binop_(nt)}) = ((binop = ibinop_1) \/ $in_binop(nt, binop, ibinop'*{ibinop' : binop_(nt)}))
-}
-
-;; 6-typing.watsup
-rec {
-
-;; 6-typing.watsup:1157.1-1157.63
-def $in_numtype(numtype : numtype, numtype*) : bool
-  ;; 6-typing.watsup:1158.1-1158.33
-  def $in_numtype{nt : numtype}(nt, []) = false
-  ;; 6-typing.watsup:1159.1-1159.68
-  def $in_numtype{nt : numtype, nt_1 : numtype, nt'* : numtype*}(nt, [nt_1] :: nt'*{nt' : numtype}) = ((nt = nt_1) \/ $in_numtype(nt, nt'*{nt' : numtype}))
-}
-
 ;; 6-typing.watsup
 relation Instr_const: `%|-%CONST`(context, instr)
   ;; 6-typing.watsup
@@ -4720,8 +4698,8 @@ relation Instr_const: `%|-%CONST`(context, instr)
   ;; 6-typing.watsup
   rule binop{C : context, Inn : Inn, binop : binop_((Inn : Inn <: numtype))}:
     `%|-%CONST`(C, BINOP_instr((Inn : Inn <: numtype), binop))
-    -- if $in_numtype((Inn : Inn <: numtype), [I32_numtype I64_numtype])
-    -- if $in_binop((Inn : Inn <: numtype), binop, [ADD_binop_ SUB_binop_ MUL_binop_])
+    -- if Inn <- [I32_Inn I64_Inn]
+    -- if binop <- [ADD_binop_ SUB_binop_ MUL_binop_]
 
 ;; 6-typing.watsup
 relation Expr_const: `%|-%CONST`(context, expr)
@@ -4884,13 +4862,13 @@ relation Export_ok: `%|-%:%`(context, export, externtype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1306.1-1306.100
+;; 6-typing.watsup:1297.1-1297.100
 relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
-  ;; 6-typing.watsup:1348.1-1349.17
+  ;; 6-typing.watsup:1339.1-1340.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1351.1-1354.55
+  ;; 6-typing.watsup:1342.1-1345.55
   rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}:
     `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype})
     -- Global_ok: `%|-%:%`(C, global, gt_1)
@@ -4900,13 +4878,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1305.1-1305.98
+;; 6-typing.watsup:1296.1-1296.98
 relation Types_ok: `%|-%:%`(context, type*, deftype*)
-  ;; 6-typing.watsup:1340.1-1341.17
+  ;; 6-typing.watsup:1331.1-1332.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1343.1-1346.50
+  ;; 6-typing.watsup:1334.1-1337.50
   rule cons{C : context, type_1 : type, type* : type*, dt_1* : deftype*, dt* : deftype*}:
     `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{dt_1 : deftype} :: dt*{dt : deftype})
     -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype})
@@ -10645,11 +10623,11 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
     `%|-%:%`(C, REF.NULL_instr(ht), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(`NULL%?`_nul(?(())), ht)])))
     -- Heaptype_ok: `%|-%:OK`(C, ht)
 
-  ;; 6-typing.watsup:741.1-744.29
-  rule ref.func{C : context, x : idx, dt : deftype, x_1* : idx*, x_2* : idx*}:
+  ;; 6-typing.watsup:741.1-744.20
+  rule ref.func{C : context, x : idx, dt : deftype}:
     `%|-%:%`(C, REF.FUNC_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(`NULL%?`_nul(?()), (dt : deftype <: heaptype))])))
     -- if (C.FUNCS_context[x!`%`_idx.0] = dt)
-    -- if (C.REFS_context = x_1*{x_1 : funcidx} :: [x] :: x_2*{x_2 : funcidx})
+    -- if x <- C.REFS_context
 
   ;; 6-typing.watsup:746.1-747.34
   rule ref.i31{C : context}:
@@ -11075,28 +11053,6 @@ relation Expr_ok: `%|-%:%`(context, expr, resulttype)
     `%|-%:%`(C, instr*{instr : instr}, `%`_resulttype(t*{t : valtype}))
     -- Instrs_ok: `%|-%:%`(C, instr*{instr : instr}, `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype(t*{t : valtype})))
 
-;; 6-typing.watsup
-rec {
-
-;; 6-typing.watsup:1161.1-1161.86
-def $in_binop(numtype : numtype, binop_ : binop_(numtype), binop_(numtype)*) : bool
-  ;; 6-typing.watsup:1162.1-1162.38
-  def $in_binop{nt : numtype, binop : binop_(nt)}(nt, binop, []) = false
-  ;; 6-typing.watsup:1163.1-1163.99
-  def $in_binop{nt : numtype, binop : binop_(nt), ibinop_1 : binop_(nt), ibinop'* : binop_(nt)*}(nt, binop, [ibinop_1] :: ibinop'*{ibinop' : binop_(nt)}) = ((binop = ibinop_1) \/ $in_binop(nt, binop, ibinop'*{ibinop' : binop_(nt)}))
-}
-
-;; 6-typing.watsup
-rec {
-
-;; 6-typing.watsup:1157.1-1157.63
-def $in_numtype(numtype : numtype, numtype*) : bool
-  ;; 6-typing.watsup:1158.1-1158.33
-  def $in_numtype{nt : numtype}(nt, []) = false
-  ;; 6-typing.watsup:1159.1-1159.68
-  def $in_numtype{nt : numtype, nt_1 : numtype, nt'* : numtype*}(nt, [nt_1] :: nt'*{nt' : numtype}) = ((nt = nt_1) \/ $in_numtype(nt, nt'*{nt' : numtype}))
-}
-
 ;; 6-typing.watsup
 relation Instr_const: `%|-%CONST`(context, instr)
   ;; 6-typing.watsup
@@ -11155,8 +11111,8 @@ relation Instr_const: `%|-%CONST`(context, instr)
   ;; 6-typing.watsup
   rule binop{C : context, Inn : Inn, binop : binop_((Inn : Inn <: numtype))}:
     `%|-%CONST`(C, BINOP_instr((Inn : Inn <: numtype), binop))
-    -- if $in_numtype((Inn : Inn <: numtype), [I32_numtype I64_numtype])
-    -- if $in_binop((Inn : Inn <: numtype), binop, [ADD_binop_ SUB_binop_ MUL_binop_])
+    -- if Inn <- [I32_Inn I64_Inn]
+    -- if binop <- [ADD_binop_ SUB_binop_ MUL_binop_]
 
 ;; 6-typing.watsup
 relation Expr_const: `%|-%CONST`(context, expr)
@@ -11319,13 +11275,13 @@ relation Export_ok: `%|-%:%`(context, export, externtype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1306.1-1306.100
+;; 6-typing.watsup:1297.1-1297.100
 relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
-  ;; 6-typing.watsup:1348.1-1349.17
+  ;; 6-typing.watsup:1339.1-1340.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1351.1-1354.55
+  ;; 6-typing.watsup:1342.1-1345.55
   rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}:
     `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype})
     -- Global_ok: `%|-%:%`(C, global, gt_1)
@@ -11335,13 +11291,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1305.1-1305.98
+;; 6-typing.watsup:1296.1-1296.98
 relation Types_ok: `%|-%:%`(context, type*, deftype*)
-  ;; 6-typing.watsup:1340.1-1341.17
+  ;; 6-typing.watsup:1331.1-1332.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1343.1-1346.50
+  ;; 6-typing.watsup:1334.1-1337.50
   rule cons{C : context, type_1 : type, type* : type*, dt_1* : deftype*, dt* : deftype*}:
     `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{dt_1 : deftype} :: dt*{dt : deftype})
     -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype})
@@ -17080,11 +17036,11 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
     `%|-%:%`(C, REF.NULL_instr(ht), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(`NULL%?`_nul(?(())), ht)])))
     -- Heaptype_ok: `%|-%:OK`(C, ht)
 
-  ;; 6-typing.watsup:741.1-744.29
-  rule ref.func{C : context, x : idx, dt : deftype, x_1* : idx*, x_2* : idx*}:
+  ;; 6-typing.watsup:741.1-744.20
+  rule ref.func{C : context, x : idx, dt : deftype}:
     `%|-%:%`(C, REF.FUNC_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(`NULL%?`_nul(?()), (dt : deftype <: heaptype))])))
     -- if (C.FUNCS_context[x!`%`_idx.0] = dt)
-    -- if (C.REFS_context = x_1*{x_1 : funcidx} :: [x] :: x_2*{x_2 : funcidx})
+    -- if x <- C.REFS_context
 
   ;; 6-typing.watsup:746.1-747.34
   rule ref.i31{C : context}:
@@ -17510,28 +17466,6 @@ relation Expr_ok: `%|-%:%`(context, expr, resulttype)
     `%|-%:%`(C, instr*{instr : instr}, `%`_resulttype(t*{t : valtype}))
     -- Instrs_ok: `%|-%:%`(C, instr*{instr : instr}, `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype(t*{t : valtype})))
 
-;; 6-typing.watsup
-rec {
-
-;; 6-typing.watsup:1161.1-1161.86
-def $in_binop(numtype : numtype, binop_ : binop_(numtype), binop_(numtype)*) : bool
-  ;; 6-typing.watsup:1162.1-1162.38
-  def $in_binop{nt : numtype, binop : binop_(nt)}(nt, binop, []) = false
-  ;; 6-typing.watsup:1163.1-1163.99
-  def $in_binop{nt : numtype, binop : binop_(nt), ibinop_1 : binop_(nt), ibinop'* : binop_(nt)*}(nt, binop, [ibinop_1] :: ibinop'*{ibinop' : binop_(nt)}) = ((binop = ibinop_1) \/ $in_binop(nt, binop, ibinop'*{ibinop' : binop_(nt)}))
-}
-
-;; 6-typing.watsup
-rec {
-
-;; 6-typing.watsup:1157.1-1157.63
-def $in_numtype(numtype : numtype, numtype*) : bool
-  ;; 6-typing.watsup:1158.1-1158.33
-  def $in_numtype{nt : numtype}(nt, []) = false
-  ;; 6-typing.watsup:1159.1-1159.68
-  def $in_numtype{nt : numtype, nt_1 : numtype, nt'* : numtype*}(nt, [nt_1] :: nt'*{nt' : numtype}) = ((nt = nt_1) \/ $in_numtype(nt, nt'*{nt' : numtype}))
-}
-
 ;; 6-typing.watsup
 relation Instr_const: `%|-%CONST`(context, instr)
   ;; 6-typing.watsup
@@ -17590,8 +17524,8 @@ relation Instr_const: `%|-%CONST`(context, instr)
   ;; 6-typing.watsup
   rule binop{C : context, Inn : Inn, binop : binop_((Inn : Inn <: numtype))}:
     `%|-%CONST`(C, BINOP_instr((Inn : Inn <: numtype), binop))
-    -- if $in_numtype((Inn : Inn <: numtype), [I32_numtype I64_numtype])
-    -- if $in_binop((Inn : Inn <: numtype), binop, [ADD_binop_ SUB_binop_ MUL_binop_])
+    -- if Inn <- [I32_Inn I64_Inn]
+    -- if binop <- [ADD_binop_ SUB_binop_ MUL_binop_]
 
 ;; 6-typing.watsup
 relation Expr_const: `%|-%CONST`(context, expr)
@@ -17754,13 +17688,13 @@ relation Export_ok: `%|-%:%`(context, export, externtype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1306.1-1306.100
+;; 6-typing.watsup:1297.1-1297.100
 relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
-  ;; 6-typing.watsup:1348.1-1349.17
+  ;; 6-typing.watsup:1339.1-1340.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1351.1-1354.55
+  ;; 6-typing.watsup:1342.1-1345.55
   rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}:
     `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype})
     -- Global_ok: `%|-%:%`(C, global, gt_1)
@@ -17770,13 +17704,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1305.1-1305.98
+;; 6-typing.watsup:1296.1-1296.98
 relation Types_ok: `%|-%:%`(context, type*, deftype*)
-  ;; 6-typing.watsup:1340.1-1341.17
+  ;; 6-typing.watsup:1331.1-1332.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1343.1-1346.50
+  ;; 6-typing.watsup:1334.1-1337.50
   rule cons{C : context, type_1 : type, type* : type*, dt_1* : deftype*, dt* : deftype*}:
     `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{dt_1 : deftype} :: dt*{dt : deftype})
     -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype})
@@ -23550,12 +23484,12 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
     `%|-%:%`(C, REF.NULL_instr(ht), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(`NULL%?`_nul(?(())), ht)])))
     -- Heaptype_ok: `%|-%:OK`(C, ht)
 
-  ;; 6-typing.watsup:741.1-744.29
-  rule ref.func{C : context, x : idx, dt : deftype, x_1* : idx*, x_2* : idx*}:
+  ;; 6-typing.watsup:741.1-744.20
+  rule ref.func{C : context, x : idx, dt : deftype}:
     `%|-%:%`(C, REF.FUNC_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(`NULL%?`_nul(?()), (dt : deftype <: heaptype))])))
     -- if (x!`%`_idx.0 < |C.FUNCS_context|)
     -- if (C.FUNCS_context[x!`%`_idx.0] = dt)
-    -- if (C.REFS_context = x_1*{x_1 : funcidx} :: [x] :: x_2*{x_2 : funcidx})
+    -- if x <- C.REFS_context
 
   ;; 6-typing.watsup:746.1-747.34
   rule ref.i31{C : context}:
@@ -24044,28 +23978,6 @@ relation Expr_ok: `%|-%:%`(context, expr, resulttype)
     `%|-%:%`(C, instr*{instr : instr}, `%`_resulttype(t*{t : valtype}))
     -- Instrs_ok: `%|-%:%`(C, instr*{instr : instr}, `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype(t*{t : valtype})))
 
-;; 6-typing.watsup
-rec {
-
-;; 6-typing.watsup:1161.1-1161.86
-def $in_binop(numtype : numtype, binop_ : binop_(numtype), binop_(numtype)*) : bool
-  ;; 6-typing.watsup:1162.1-1162.38
-  def $in_binop{nt : numtype, binop : binop_(nt)}(nt, binop, []) = false
-  ;; 6-typing.watsup:1163.1-1163.99
-  def $in_binop{nt : numtype, binop : binop_(nt), ibinop_1 : binop_(nt), ibinop'* : binop_(nt)*}(nt, binop, [ibinop_1] :: ibinop'*{ibinop' : binop_(nt)}) = ((binop = ibinop_1) \/ $in_binop(nt, binop, ibinop'*{ibinop' : binop_(nt)}))
-}
-
-;; 6-typing.watsup
-rec {
-
-;; 6-typing.watsup:1157.1-1157.63
-def $in_numtype(numtype : numtype, numtype*) : bool
-  ;; 6-typing.watsup:1158.1-1158.33
-  def $in_numtype{nt : numtype}(nt, []) = false
-  ;; 6-typing.watsup:1159.1-1159.68
-  def $in_numtype{nt : numtype, nt_1 : numtype, nt'* : numtype*}(nt, [nt_1] :: nt'*{nt' : numtype}) = ((nt = nt_1) \/ $in_numtype(nt, nt'*{nt' : numtype}))
-}
-
 ;; 6-typing.watsup
 relation Instr_const: `%|-%CONST`(context, instr)
   ;; 6-typing.watsup
@@ -24125,8 +24037,8 @@ relation Instr_const: `%|-%CONST`(context, instr)
   ;; 6-typing.watsup
   rule binop{C : context, Inn : Inn, binop : binop_((Inn : Inn <: numtype))}:
     `%|-%CONST`(C, BINOP_instr((Inn : Inn <: numtype), binop))
-    -- if $in_numtype((Inn : Inn <: numtype), [I32_numtype I64_numtype])
-    -- if $in_binop((Inn : Inn <: numtype), binop, [ADD_binop_ SUB_binop_ MUL_binop_])
+    -- if Inn <- [I32_Inn I64_Inn]
+    -- if binop <- [ADD_binop_ SUB_binop_ MUL_binop_]
 
 ;; 6-typing.watsup
 relation Expr_const: `%|-%CONST`(context, expr)
@@ -24298,13 +24210,13 @@ relation Export_ok: `%|-%:%`(context, export, externtype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1306.1-1306.100
+;; 6-typing.watsup:1297.1-1297.100
 relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
-  ;; 6-typing.watsup:1348.1-1349.17
+  ;; 6-typing.watsup:1339.1-1340.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1351.1-1354.55
+  ;; 6-typing.watsup:1342.1-1345.55
   rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}:
     `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype})
     -- Global_ok: `%|-%:%`(C, global, gt_1)
@@ -24314,13 +24226,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1305.1-1305.98
+;; 6-typing.watsup:1296.1-1296.98
 relation Types_ok: `%|-%:%`(context, type*, deftype*)
-  ;; 6-typing.watsup:1340.1-1341.17
+  ;; 6-typing.watsup:1331.1-1332.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1343.1-1346.50
+  ;; 6-typing.watsup:1334.1-1337.50
   rule cons{C : context, type_1 : type, type* : type*, dt_1* : deftype*, dt* : deftype*}:
     `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{dt_1 : deftype} :: dt*{dt : deftype})
     -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype})
@@ -30162,12 +30074,12 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
     `%|-%:%`(C, REF.NULL_instr(ht), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(`NULL%?`_nul(?(())), ht)])))
     -- Heaptype_ok: `%|-%:OK`(C, ht)
 
-  ;; 6-typing.watsup:741.1-744.29
-  rule ref.func{C : context, x : idx, dt : deftype, x_1* : idx*, x_2* : idx*}:
+  ;; 6-typing.watsup:741.1-744.20
+  rule ref.func{C : context, x : idx, dt : deftype}:
     `%|-%:%`(C, REF.FUNC_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(`NULL%?`_nul(?()), (dt : deftype <: heaptype))])))
     -- if (x!`%`_idx.0 < |C.FUNCS_context|)
+    -- if x <- C.REFS_context
     -- where dt = C.FUNCS_context[x!`%`_idx.0]
-    -- where x_1*{x_1 : funcidx} :: [x] :: x_2*{x_2 : funcidx} = C.REFS_context
 
   ;; 6-typing.watsup:746.1-747.34
   rule ref.i31{C : context}:
@@ -30674,28 +30586,6 @@ relation Expr_ok: `%|-%:%`(context, expr, resulttype)
     `%|-%:%`(C, instr*{instr : instr}, `%`_resulttype(t*{t : valtype}))
     -- Instrs_ok: `%|-%:%`(C, instr*{instr : instr}, `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype(t*{t : valtype})))
 
-;; 6-typing.watsup
-rec {
-
-;; 6-typing.watsup:1161.1-1161.86
-def $in_binop(numtype : numtype, binop_ : binop_(numtype), binop_(numtype)*) : bool
-  ;; 6-typing.watsup:1162.1-1162.38
-  def $in_binop{nt : numtype, binop : binop_(nt)}(nt, binop, []) = false
-  ;; 6-typing.watsup:1163.1-1163.99
-  def $in_binop{nt : numtype, binop : binop_(nt), ibinop_1 : binop_(nt), ibinop'* : binop_(nt)*}(nt, binop, [ibinop_1] :: ibinop'*{ibinop' : binop_(nt)}) = ((binop = ibinop_1) \/ $in_binop(nt, binop, ibinop'*{ibinop' : binop_(nt)}))
-}
-
-;; 6-typing.watsup
-rec {
-
-;; 6-typing.watsup:1157.1-1157.63
-def $in_numtype(numtype : numtype, numtype*) : bool
-  ;; 6-typing.watsup:1158.1-1158.33
-  def $in_numtype{nt : numtype}(nt, []) = false
-  ;; 6-typing.watsup:1159.1-1159.68
-  def $in_numtype{nt : numtype, nt_1 : numtype, nt'* : numtype*}(nt, [nt_1] :: nt'*{nt' : numtype}) = ((nt = nt_1) \/ $in_numtype(nt, nt'*{nt' : numtype}))
-}
-
 ;; 6-typing.watsup
 relation Instr_const: `%|-%CONST`(context, instr)
   ;; 6-typing.watsup
@@ -30755,8 +30645,8 @@ relation Instr_const: `%|-%CONST`(context, instr)
   ;; 6-typing.watsup
   rule binop{C : context, Inn : Inn, binop : binop_((Inn : Inn <: numtype))}:
     `%|-%CONST`(C, BINOP_instr((Inn : Inn <: numtype), binop))
-    -- if $in_numtype((Inn : Inn <: numtype), [I32_numtype I64_numtype])
-    -- if $in_binop((Inn : Inn <: numtype), binop, [ADD_binop_ SUB_binop_ MUL_binop_])
+    -- if Inn <- [I32_Inn I64_Inn]
+    -- if binop <- [ADD_binop_ SUB_binop_ MUL_binop_]
 
 ;; 6-typing.watsup
 relation Expr_const: `%|-%CONST`(context, expr)
@@ -30928,13 +30818,13 @@ relation Export_ok: `%|-%:%`(context, export, externtype)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1306.1-1306.100
+;; 6-typing.watsup:1297.1-1297.100
 relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
-  ;; 6-typing.watsup:1348.1-1349.17
+  ;; 6-typing.watsup:1339.1-1340.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1351.1-1354.55
+  ;; 6-typing.watsup:1342.1-1345.55
   rule cons{C : context, global_1 : global, global : global, gt_1 : globaltype, gt* : globaltype*}:
     `%|-%:%`(C, [global_1] :: global*{}, [gt_1] :: gt*{gt : globaltype})
     -- Global_ok: `%|-%:%`(C, global, gt_1)
@@ -30944,13 +30834,13 @@ relation Globals_ok: `%|-%:%`(context, global*, globaltype*)
 ;; 6-typing.watsup
 rec {
 
-;; 6-typing.watsup:1305.1-1305.98
+;; 6-typing.watsup:1296.1-1296.98
 relation Types_ok: `%|-%:%`(context, type*, deftype*)
-  ;; 6-typing.watsup:1340.1-1341.17
+  ;; 6-typing.watsup:1331.1-1332.17
   rule empty{C : context}:
     `%|-%:%`(C, [], [])
 
-  ;; 6-typing.watsup:1343.1-1346.50
+  ;; 6-typing.watsup:1334.1-1337.50
   rule cons{C : context, type_1 : type, type* : type*, dt_1* : deftype*, dt* : deftype*}:
     `%|-%:%`(C, [type_1] :: type*{type : type}, dt_1*{dt_1 : deftype} :: dt*{dt : deftype})
     -- Type_ok: `%|-%:%`(C, type_1, dt_1*{dt_1 : deftype})
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
index 087163d427..e576c2f030 100644
--- a/spectec/test-prose/TEST.md
+++ b/spectec/test-prose/TEST.md
@@ -3816,8 +3816,8 @@ validation_of_REF.NULL ht
 
 validation_of_REF.FUNC x
 - |C.FUNCS| must be greater than x.
+- x must be contained in C.REFS.
 - Let dt be C.FUNCS[x].
-- Let x_1* ++ [x] ++ x_2* be C.REFS.
 - The instruction is valid with type ([] ->_ [] ++ [(REF (NULL ?()) dt)]).
 
 validation_of_REF.I31
@@ -6169,18 +6169,6 @@ unrollht C heapt_u0
 4. Let (REC i) be heapt_u0.
 5. Return C.RECS[i].
 
-in_binop nt binop binop_u0*
-1. If (binop_u0* is []), then:
-  a. Return false.
-2. Let [ibinop_1] ++ ibinop'* be binop_u0*.
-3. Return ((binop is ibinop_1) or $in_binop(nt, binop, ibinop'*)).
-
-in_numtype nt numty_u0*
-1. If (numty_u0* is []), then:
-  a. Return false.
-2. Let [nt_1] ++ nt'* be numty_u0*.
-3. Return ((nt is nt_1) or $in_numtype(nt, nt'*)).
-
 funcidx_nonfuncs YetE (`%%%%%`_nonfuncs(global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data}))
 1. Return $funcidx_module((MODULE [] [] [] global* table* mem* elem* data* [] [])).
 
diff --git a/spectec/test-prose/doc/valid/instructions-in.rst b/spectec/test-prose/doc/valid/instructions-in.rst
index 47ab5071bf..d4c4896d46 100644
--- a/spectec/test-prose/doc/valid/instructions-in.rst
+++ b/spectec/test-prose/doc/valid/instructions-in.rst
@@ -871,19 +871,3 @@ $${rule+:
   Expr_const
   Expr_ok_const
 }
-
-.. _def-in_binop:
-
-$${definition-prose: in_binop}
-
-\
-
-$${definition: in_binop}
-
-.. _def-in_numtype:
-
-$${definition-prose: in_numtype}
-
-\
-
-$${definition: in_numtype}
diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md
index 480ecd1711..dc536b3ad3 100644
--- a/spectec/test-splice/TEST.md
+++ b/spectec/test-splice/TEST.md
@@ -1317,8 +1317,6 @@ warning: definition `ilt` was never spliced
 warning: definition `imax` was never spliced
 warning: definition `imin` was never spliced
 warning: definition `imul` was never spliced
-warning: definition `in_binop` was never spliced
-warning: definition `in_numtype` was never spliced
 warning: definition `ine` was never spliced
 warning: definition `ineg` was never spliced
 warning: definition `inot` was never spliced
@@ -1799,8 +1797,6 @@ warning: definition prose `growmem` was never spliced
 warning: definition prose `growtable` was never spliced
 warning: definition prose `half` was never spliced
 warning: definition prose `idx` was never spliced
-warning: definition prose `in_binop` was never spliced
-warning: definition prose `in_numtype` was never spliced
 warning: definition prose `inst_reftype` was never spliced
 warning: definition prose `inst_valtype` was never spliced
 warning: definition prose `instantiate` was never spliced