diff --git a/specification/wasm-3.0/2.1-validation.types.spectec b/specification/wasm-3.0/2.1-validation.types.spectec
index 9cb88dc0a7..916474232d 100644
--- a/specification/wasm-3.0/2.1-validation.types.spectec
+++ b/specification/wasm-3.0/2.1-validation.types.spectec
@@ -85,9 +85,9 @@ rule Expand_use/typeidx: _IDX typeidx ~~_C comptype  -- Expand: C.TYPES[typeidx]
 ;; Type definitions
 
 syntax oktypeidx hint(show OK#((typeidx))) hint(prose_desc "type index") =
-  | OK typeidx      hint(show OK#(%))     hint(macro "%subtype")    hint(prose "%1")
-syntax oktypeidxnat hint(show OK#(typeidx,n)) =
-  | OK typeidx nat  hint(show OK#(%,%))   hint(macro "%subtypeext")
+  | OK typeidx   hint(show OK#(%))      hint(macro "%subtype") hint(prose "%1")
+syntax oktypenat hint(show OK#(n)) =
+  | OK nat       hint(show OK#(%))      hint(macro "%subtypeext")
 
 relation Packtype_ok: context |- packtype : OK          hint(name "K-pack")    hint(macro "%packtype")
 relation Fieldtype_ok: context |- fieldtype : OK        hint(name "K-field")   hint(macro "%fieldtype")
@@ -95,8 +95,8 @@ relation Storagetype_ok: context |- storagetype : OK    hint(name "K-storage") h
 relation Comptype_ok: context |- comptype : OK          hint(name "K-comp")    hint(macro "%comptype")
 relation Subtype_ok: context |- subtype : oktypeidx     hint(name "K-sub")     hint(macro "%subtype")     hint(prosepp "for")
 relation Rectype_ok: context |- rectype : oktypeidx     hint(name "K-rect")    hint(macro "%rectype")     hint(prosepp "for")
-relation Subtype_ok2: context |- subtype : oktypeidxnat hint(name "K-sub2")    hint(macro "%subtypeext")  hint(prosepp "for")
-relation Rectype_ok2: context |- rectype : oktypeidxnat hint(name "K-rec2")    hint(macro "%rectypeext")  hint(prosepp "for")
+relation Subtype_ok2: context |- subtype : oktypenat    hint(name "K-sub2")    hint(macro "%subtypeext")  hint(prosepp "for")
+relation Rectype_ok2: context |- rectype : oktypenat    hint(name "K-rec2")    hint(macro "%rectypeext")  hint(prosepp "for")
 relation Deftype_ok: context |- deftype : OK            hint(name "K-def")     hint(macro "%deftype")
 
 ;; Forward declarations for validation.subtyping
@@ -156,10 +156,9 @@ rule Subtype_ok:
   -- Comptype_ok: C |- comptype : OK
   -- (Comptype_sub: C |- comptype <: comptype')*
 
-def $before(typeuse, typeidx, nat) : bool   hint(show % << %,%) hint(macro "before")
-def $before(deftype, x, i) = true
-def $before(_IDX typeidx, x, i) = typeidx < x
-def $before(REC j, x, i) = j < i
+def $before(typeuse, nat) : bool   hint(show % << %) hint(macro "before")
+def $before(REC j, i) = j < i
+def $before(typeuse, i) = true  -- otherwise
 
 def $unrollht(context, heaptype) : subtype  hint(show $unroll_(%,%))
 def $unrollht(C, deftype) = $unrolldt(deftype)
@@ -167,10 +166,10 @@ def $unrollht(C, _IDX typeidx) = $unrolldt(C.TYPES[typeidx])
 def $unrollht(C, REC i) = C.RECS[i]
 
 rule Subtype_ok2:
-  C |- SUB FINAL? typeuse* comptype : OK x i
+  C |- SUB FINAL? typeuse* comptype : OK(i)
   -- if |typeuse*| <= 1
   -- (Typeuse_ok: C |- typeuse : OK)*
-  -- (if $before(typeuse, x, i))*
+  -- (if $before(typeuse, i))*
   -- (if $unrollht(C, typeuse) = SUB typeuse'* comptype')*
   ----
   -- Comptype_ok: C |- comptype : OK
@@ -187,17 +186,17 @@ rule Rectype_ok/cons:
 
 
 rule Rectype_ok2/empty:
-  C |- REC eps : OK x i
+  C |- REC eps : OK(i)
 
 rule Rectype_ok2/cons:
-  C |- REC (subtype_1 subtype*) : OK x i
-  -- Subtype_ok2: C |- subtype_1 : OK x i
-  -- Rectype_ok2: C |- REC subtype* : OK x $(i+1)
+  C |- REC (subtype_1 subtype*) : OK(i)
+  -- Subtype_ok2: C |- subtype_1 : OK(i)
+  -- Rectype_ok2: C |- REC subtype* : OK($(i+1))
 
 
 rule Deftype_ok:
   C |- _DEF rectype i : OK
-  -- Rectype_ok2: C, RECS subtype^n |- rectype : OK x 0
+  -- Rectype_ok2: C, RECS subtype^n |- rectype : OK(0)
   -- if rectype = REC subtype^n
   -- if i < n
 
diff --git a/specification/wasm-3.0/7.0-soundness.contexts.spectec b/specification/wasm-3.0/7.0-soundness.contexts.spectec
index fcddfe5bb1..420fcf7c7e 100644
--- a/specification/wasm-3.0/7.0-soundness.contexts.spectec
+++ b/specification/wasm-3.0/7.0-soundness.contexts.spectec
@@ -21,7 +21,7 @@ rule Context_ok:
     }
   -- if C_0 = {TYPES dt^n}
   -- (Deftype_ok: {TYPES dt^n[0 : i]} |- dt : OK)^(i<n)
-  -- (Subtype_ok2: {TYPES dt^n, RECS st^m} |- st : OK n i)^(i<m)
+  -- (Subtype_ok2: {TYPES dt^n, RECS st^m} |- st : OK(i))^(i<m)
   -- (Tagtype_ok: C_0 |- jt : OK)*
   -- (Globaltype_ok: C_0 |- gt : OK)*
   -- (Memtype_ok: C_0 |- mt : OK)*
diff --git a/specification/wasm-latest/2.1-validation.types.spectec b/specification/wasm-latest/2.1-validation.types.spectec
index 9cb88dc0a7..916474232d 100644
--- a/specification/wasm-latest/2.1-validation.types.spectec
+++ b/specification/wasm-latest/2.1-validation.types.spectec
@@ -85,9 +85,9 @@ rule Expand_use/typeidx: _IDX typeidx ~~_C comptype  -- Expand: C.TYPES[typeidx]
 ;; Type definitions
 
 syntax oktypeidx hint(show OK#((typeidx))) hint(prose_desc "type index") =
-  | OK typeidx      hint(show OK#(%))     hint(macro "%subtype")    hint(prose "%1")
-syntax oktypeidxnat hint(show OK#(typeidx,n)) =
-  | OK typeidx nat  hint(show OK#(%,%))   hint(macro "%subtypeext")
+  | OK typeidx   hint(show OK#(%))      hint(macro "%subtype") hint(prose "%1")
+syntax oktypenat hint(show OK#(n)) =
+  | OK nat       hint(show OK#(%))      hint(macro "%subtypeext")
 
 relation Packtype_ok: context |- packtype : OK          hint(name "K-pack")    hint(macro "%packtype")
 relation Fieldtype_ok: context |- fieldtype : OK        hint(name "K-field")   hint(macro "%fieldtype")
@@ -95,8 +95,8 @@ relation Storagetype_ok: context |- storagetype : OK    hint(name "K-storage") h
 relation Comptype_ok: context |- comptype : OK          hint(name "K-comp")    hint(macro "%comptype")
 relation Subtype_ok: context |- subtype : oktypeidx     hint(name "K-sub")     hint(macro "%subtype")     hint(prosepp "for")
 relation Rectype_ok: context |- rectype : oktypeidx     hint(name "K-rect")    hint(macro "%rectype")     hint(prosepp "for")
-relation Subtype_ok2: context |- subtype : oktypeidxnat hint(name "K-sub2")    hint(macro "%subtypeext")  hint(prosepp "for")
-relation Rectype_ok2: context |- rectype : oktypeidxnat hint(name "K-rec2")    hint(macro "%rectypeext")  hint(prosepp "for")
+relation Subtype_ok2: context |- subtype : oktypenat    hint(name "K-sub2")    hint(macro "%subtypeext")  hint(prosepp "for")
+relation Rectype_ok2: context |- rectype : oktypenat    hint(name "K-rec2")    hint(macro "%rectypeext")  hint(prosepp "for")
 relation Deftype_ok: context |- deftype : OK            hint(name "K-def")     hint(macro "%deftype")
 
 ;; Forward declarations for validation.subtyping
@@ -156,10 +156,9 @@ rule Subtype_ok:
   -- Comptype_ok: C |- comptype : OK
   -- (Comptype_sub: C |- comptype <: comptype')*
 
-def $before(typeuse, typeidx, nat) : bool   hint(show % << %,%) hint(macro "before")
-def $before(deftype, x, i) = true
-def $before(_IDX typeidx, x, i) = typeidx < x
-def $before(REC j, x, i) = j < i
+def $before(typeuse, nat) : bool   hint(show % << %) hint(macro "before")
+def $before(REC j, i) = j < i
+def $before(typeuse, i) = true  -- otherwise
 
 def $unrollht(context, heaptype) : subtype  hint(show $unroll_(%,%))
 def $unrollht(C, deftype) = $unrolldt(deftype)
@@ -167,10 +166,10 @@ def $unrollht(C, _IDX typeidx) = $unrolldt(C.TYPES[typeidx])
 def $unrollht(C, REC i) = C.RECS[i]
 
 rule Subtype_ok2:
-  C |- SUB FINAL? typeuse* comptype : OK x i
+  C |- SUB FINAL? typeuse* comptype : OK(i)
   -- if |typeuse*| <= 1
   -- (Typeuse_ok: C |- typeuse : OK)*
-  -- (if $before(typeuse, x, i))*
+  -- (if $before(typeuse, i))*
   -- (if $unrollht(C, typeuse) = SUB typeuse'* comptype')*
   ----
   -- Comptype_ok: C |- comptype : OK
@@ -187,17 +186,17 @@ rule Rectype_ok/cons:
 
 
 rule Rectype_ok2/empty:
-  C |- REC eps : OK x i
+  C |- REC eps : OK(i)
 
 rule Rectype_ok2/cons:
-  C |- REC (subtype_1 subtype*) : OK x i
-  -- Subtype_ok2: C |- subtype_1 : OK x i
-  -- Rectype_ok2: C |- REC subtype* : OK x $(i+1)
+  C |- REC (subtype_1 subtype*) : OK(i)
+  -- Subtype_ok2: C |- subtype_1 : OK(i)
+  -- Rectype_ok2: C |- REC subtype* : OK($(i+1))
 
 
 rule Deftype_ok:
   C |- _DEF rectype i : OK
-  -- Rectype_ok2: C, RECS subtype^n |- rectype : OK x 0
+  -- Rectype_ok2: C, RECS subtype^n |- rectype : OK(0)
   -- if rectype = REC subtype^n
   -- if i < n
 
diff --git a/specification/wasm-latest/7.0-soundness.contexts.spectec b/specification/wasm-latest/7.0-soundness.contexts.spectec
index fcddfe5bb1..420fcf7c7e 100644
--- a/specification/wasm-latest/7.0-soundness.contexts.spectec
+++ b/specification/wasm-latest/7.0-soundness.contexts.spectec
@@ -21,7 +21,7 @@ rule Context_ok:
     }
   -- if C_0 = {TYPES dt^n}
   -- (Deftype_ok: {TYPES dt^n[0 : i]} |- dt : OK)^(i<n)
-  -- (Subtype_ok2: {TYPES dt^n, RECS st^m} |- st : OK n i)^(i<m)
+  -- (Subtype_ok2: {TYPES dt^n, RECS st^m} |- st : OK(i))^(i<m)
   -- (Tagtype_ok: C_0 |- jt : OK)*
   -- (Globaltype_ok: C_0 |- gt : OK)*
   -- (Memtype_ok: C_0 |- mt : OK)*
diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf
index 68bdcbc000..4722e81f4d 100644
Binary files a/spectec/doc/example/output/NanoWasm.pdf and b/spectec/doc/example/output/NanoWasm.pdf differ
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index 4c0e2bfd15..7f1a22bac6 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -2722,8 +2722,8 @@ relation Vectype_ok: `%|-%:OK`(context, vectype)
     `%|-%:OK`(C, vectype)
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-syntax oktypeidxnat =
-  | OK(typeidx : typeidx, nat)
+syntax oktypenat =
+  | OK(nat)
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
 relation Packtype_ok: `%|-%:OK`(context, packtype)
@@ -2757,13 +2757,12 @@ relation Vectype_sub: `%|-%<:%`(context, vectype, vectype)
     `%|-%<:%`(C, vectype, vectype)
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-def $before(typeuse : typeuse, typeidx : typeidx, nat : nat) : bool
+def $before(typeuse : typeuse, nat : nat) : bool
   ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-  def $before{deftype : deftype, x : idx, i : nat}((deftype : deftype <: typeuse), x, i) = true
+  def $before{j : n, i : nat}(REC_typeuse(j), i) = (j < i)
   ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-  def $before{typeidx : typeidx, x : idx, i : nat}(_IDX_typeuse(typeidx), x, i) = (typeidx!`%`_typeidx.0 < x!`%`_idx.0)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-  def $before{j : n, x : idx, i : nat}(REC_typeuse(j), x, i) = (j < i)
+  def $before{tu : typeuse, i : nat}(tu, i) = true
+    -- otherwise
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
 def $unrollht(context : context, heaptype : heaptype) : subtype
@@ -2882,35 +2881,35 @@ relation Comptype_ok: `%|-%:OK`(context, comptype)
     -- Resulttype_ok: `%|-%:OK`(C, `%`_resulttype(t_2*{t_2 <- `t_2*`}))
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:98.1-98.126
-relation Subtype_ok2: `%|-%:%`(context, subtype, oktypeidxnat)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:169.1-177.49
-  rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, x : idx, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
-    `%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypeidxnat(x, i))
+relation Subtype_ok2: `%|-%:%`(context, subtype, oktypenat)
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:168.1-176.49
+  rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
+    `%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypenat(i))
     -- if (|typeuse*{typeuse <- `typeuse*`}| <= 1)
     -- (Typeuse_ok: `%|-%:OK`(C, typeuse))*{typeuse <- `typeuse*`}
-    -- (if $before(typeuse, x, i))*{typeuse <- `typeuse*`}
+    -- (if $before(typeuse, i))*{typeuse <- `typeuse*`}
     -- (if ($unrollht(C, (typeuse : typeuse <: heaptype)) = SUB_subtype(?(), typeuse'*{typeuse' <- `typeuse'*`}, comptype')))*{comptype' <- `comptype'*`, typeuse <- `typeuse*`, `typeuse'*` <- `typeuse'**`}
     -- Comptype_ok: `%|-%:OK`(C, comptype)
     -- (Comptype_sub: `%|-%<:%`(C, comptype, comptype'))*{comptype' <- `comptype'*`}
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:99.1-99.126
-relation Rectype_ok2: `%|-%:%`(context, rectype, oktypeidxnat)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:189.1-190.24
-  rule empty{C : context, x : idx, i : nat}:
-    `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidxnat(x, i))
+relation Rectype_ok2: `%|-%:%`(context, rectype, oktypenat)
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:188.1-189.23
+  rule empty{C : context, i : nat}:
+    `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypenat(i))
 
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:192.1-195.50
-  rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx, i : nat}:
-    `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, i))
-    -- Subtype_ok2: `%|-%:%`(C, subtype_1, OK_oktypeidxnat(x, i))
-    -- Rectype_ok2: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, (i + 1)))
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:191.1-194.49
+  rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, i : nat}:
+    `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypenat(i))
+    -- Subtype_ok2: `%|-%:%`(C, subtype_1, OK_oktypenat(i))
+    -- Rectype_ok2: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypenat((i + 1)))
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:100.1-100.102
 relation Deftype_ok: `%|-%:OK`(context, deftype)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:198.1-202.14
-  rule _{C : context, rectype : rectype, i : n, n : n, `subtype*` : subtype*, x : idx}:
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:197.1-201.14
+  rule _{C : context, rectype : rectype, i : n, n : n, `subtype*` : subtype*}:
     `%|-%:OK`(C, _DEF_deftype(rectype, i))
-    -- Rectype_ok2: `%|-%:%`({TYPES [], RECS subtype^n{subtype <- `subtype*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []} +++ C, rectype, OK_oktypeidxnat(x, 0))
+    -- Rectype_ok2: `%|-%:%`({TYPES [], RECS subtype^n{subtype <- `subtype*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []} +++ C, rectype, OK_oktypenat(0))
     -- if (rectype = REC_rectype(`%`_list(subtype^n{subtype <- `subtype*`})))
     -- if (i < n)
 
@@ -3151,11 +3150,11 @@ rec {
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:97.1-97.126
 relation Rectype_ok: `%|-%:%`(context, rectype, oktypeidx)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:180.1-181.23
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:179.1-180.23
   rule empty{C : context, x : idx}:
     `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidx(x))
 
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:183.1-186.48
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:182.1-185.48
   rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx}:
     `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidx(x))
     -- Subtype_ok: `%|-%:%`(C, subtype_1, OK_oktypeidx(x))
@@ -7665,7 +7664,7 @@ relation Context_ok: `|-%:OK`(context)
     -- if (C = {TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS jt*{jt <- `jt*`}, GLOBALS gt*{gt <- `gt*`}, MEMS mt*{mt <- `mt*`}, TABLES tt*{tt <- `tt*`}, FUNCS dt_F*{dt_F <- `dt_F*`}, DATAS ok*{ok <- `ok*`}, ELEMS et*{et <- `et*`}, LOCALS lct*{lct <- `lct*`}, LABELS [`%`_resulttype((rt : reftype <: valtype)*{rt <- `rt*`})], RETURN ?(`%`_resulttype(lift((rt' : reftype <: valtype)?{rt' <- `rt'?`}))), REFS x*{x <- `x*`}})
     -- if (C_0 = {TYPES dt^n{dt <- `dt*`}, RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []})
     -- (Deftype_ok: `%|-%:OK`({TYPES dt^n{dt <- `dt*`}[0 : i], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, dt))^(i<n){dt <- `dt*`}
-    -- (Subtype_ok2: `%|-%:%`({TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, st, OK_oktypeidxnat(`%`_typeidx(n), i)))^(i<m){st <- `st*`}
+    -- (Subtype_ok2: `%|-%:%`({TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, st, OK_oktypenat(i)))^(i<m){st <- `st*`}
     -- (Tagtype_ok: `%|-%:OK`(C_0, jt))*{jt <- `jt*`}
     -- (Globaltype_ok: `%|-%:OK`(C_0, gt))*{gt <- `gt*`}
     -- (Memtype_ok: `%|-%:OK`(C_0, mt))*{mt <- `mt*`}
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index 739e2ff72e..b2aa51a531 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -4769,7 +4769,7 @@ $$
 $$
 \begin{array}[t]{@{}lrrl@{}l@{}}
 & {\mathsf{ok}}{({\mathit{typeidx}})} & ::= & {\mathsf{ok}}{{\mathit{typeidx}}} \\
-& {\mathsf{ok}}{({\mathit{typeidx}}, n)} & ::= & {\mathsf{ok}}{({\mathit{typeidx}}, \mathbb{N})} \\
+& {\mathsf{ok}}{n} & ::= & {\mathsf{ok}}{\mathbb{N}} \\
 \end{array}
 $$
 
@@ -4785,9 +4785,9 @@ $\boxed{{\mathit{context}} \vdash {\mathit{subtype}} : {\mathsf{ok}}{({\mathit{t
 
 $\boxed{{\mathit{context}} \vdash {\mathit{rectype}} : {\mathsf{ok}}{({\mathit{typeidx}})}}$
 
-$\boxed{{\mathit{context}} \vdash {\mathit{subtype}} : {\mathsf{ok}}{({\mathit{typeidx}}, n)}}$
+$\boxed{{\mathit{context}} \vdash {\mathit{subtype}} : {\mathsf{ok}}{n}}$
 
-$\boxed{{\mathit{context}} \vdash {\mathit{rectype}} : {\mathsf{ok}}{({\mathit{typeidx}}, n)}}$
+$\boxed{{\mathit{context}} \vdash {\mathit{rectype}} : {\mathsf{ok}}{n}}$
 
 $\boxed{{\mathit{context}} \vdash {\mathit{deftype}} : \mathsf{ok}}$
 
@@ -4937,9 +4937,8 @@ $$
 
 $$
 \begin{array}[t]{@{}lcl@{}l@{}}
-{\mathit{deftype}} \prec x, i & = & \mathsf{true} \\
-{\mathit{typeidx}} \prec x, i & = & {\mathit{typeidx}} < x \\
-\mathsf{rec} {.} j \prec x, i & = & j < i \\
+\mathsf{rec} {.} j \prec i & = & j < i \\
+{\mathit{typeuse}} \prec i & = & \mathsf{true} & \quad \mbox{otherwise} \\
 \end{array}
 $$
 
@@ -4959,7 +4958,7 @@ $$
  \qquad
 (C \vdash {\mathit{typeuse}} : \mathsf{ok})^\ast
  \qquad
-({\mathit{typeuse}} \prec x, i)^\ast
+({\mathit{typeuse}} \prec i)^\ast
  \qquad
 ({{\mathrm{unroll}}}_{C}({\mathit{typeuse}}) = \mathsf{sub}~{{\mathit{typeuse}'}^\ast}~{\mathit{comptype}'})^\ast
  \\
@@ -4968,7 +4967,7 @@ C \vdash {\mathit{comptype}} : \mathsf{ok}
 (C \vdash {\mathit{comptype}} \leq {\mathit{comptype}'})^\ast
 \end{array}
 }{
-C \vdash \mathsf{sub}~{\mathsf{final}^?}~{{\mathit{typeuse}}^\ast}~{\mathit{comptype}} : {\mathsf{ok}}{(x, i)}
+C \vdash \mathsf{sub}~{\mathsf{final}^?}~{{\mathit{typeuse}}^\ast}~{\mathit{comptype}} : {\mathsf{ok}}{(i)}
 } \, {[\textsc{\scriptsize K{-}sub2}]}
 \qquad
 \end{array}
@@ -5005,7 +5004,7 @@ $$
 \begin{array}{@{}c@{}}\displaystyle
 \frac{
 }{
-C \vdash \mathsf{rec}~\epsilon : {\mathsf{ok}}{(x, i)}
+C \vdash \mathsf{rec}~\epsilon : {\mathsf{ok}}{(i)}
 } \, {[\textsc{\scriptsize K{-}rec2{-}empty}]}
 \qquad
 \end{array}
@@ -5014,11 +5013,11 @@ $$
 $$
 \begin{array}{@{}c@{}}\displaystyle
 \frac{
-C \vdash {\mathit{subtype}}_1 : {\mathsf{ok}}{(x, i)}
+C \vdash {\mathit{subtype}}_1 : {\mathsf{ok}}{(i)}
  \qquad
-C \vdash \mathsf{rec}~{{\mathit{subtype}}^\ast} : {\mathsf{ok}}{(x, i + 1)}
+C \vdash \mathsf{rec}~{{\mathit{subtype}}^\ast} : {\mathsf{ok}}{(i + 1)}
 }{
-C \vdash \mathsf{rec}~({\mathit{subtype}}_1~{{\mathit{subtype}}^\ast}) : {\mathsf{ok}}{(x, i)}
+C \vdash \mathsf{rec}~({\mathit{subtype}}_1~{{\mathit{subtype}}^\ast}) : {\mathsf{ok}}{(i)}
 } \, {[\textsc{\scriptsize K{-}rec2{-}cons}]}
 \qquad
 \end{array}
@@ -5029,7 +5028,7 @@ $$
 $$
 \begin{array}{@{}c@{}}\displaystyle
 \frac{
-C, \mathsf{recs}~{{\mathit{subtype}}^{n}} \vdash {\mathit{rectype}} : {\mathsf{ok}}{(x, 0)}
+C, \mathsf{recs}~{{\mathit{subtype}}^{n}} \vdash {\mathit{rectype}} : {\mathsf{ok}}{(0)}
  \qquad
 {\mathit{rectype}} = \mathsf{rec}~{{\mathit{subtype}}^{n}}
  \qquad
@@ -14045,7 +14044,7 @@ C_0 = \{ \mathsf{types}~{{\mathit{dt}}^{n}} \}
  \qquad
 (\{ \mathsf{types}~{{\mathit{dt}}^{n}}{}[0 : i] \} \vdash {\mathit{dt}} : \mathsf{ok})^{i<n}
  \qquad
-(\{ \mathsf{types}~{{\mathit{dt}}^{n}},\;\allowbreak \mathsf{recs}~{{\mathit{st}}^{m}} \} \vdash {\mathit{st}} : {\mathsf{ok}}{(n, i)})^{i<m}
+(\{ \mathsf{types}~{{\mathit{dt}}^{n}},\;\allowbreak \mathsf{recs}~{{\mathit{st}}^{m}} \} \vdash {\mathit{st}} : {\mathsf{ok}}{(i)})^{i<m}
  \qquad
 (C_0 \vdash {\mathit{jt}} : \mathsf{ok})^\ast
  \qquad
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
index 6a75185232..2aa07a8857 100644
--- a/spectec/test-middlend/TEST.md
+++ b/spectec/test-middlend/TEST.md
@@ -2712,8 +2712,8 @@ relation Vectype_ok: `%|-%:OK`(context, vectype)
     `%|-%:OK`(C, vectype)
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-syntax oktypeidxnat =
-  | OK(typeidx : typeidx, nat)
+syntax oktypenat =
+  | OK(nat)
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
 relation Packtype_ok: `%|-%:OK`(context, packtype)
@@ -2747,13 +2747,12 @@ relation Vectype_sub: `%|-%<:%`(context, vectype, vectype)
     `%|-%<:%`(C, vectype, vectype)
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-def $before(typeuse : typeuse, typeidx : typeidx, nat : nat) : bool
+def $before(typeuse : typeuse, nat : nat) : bool
   ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-  def $before{deftype : deftype, x : idx, i : nat}((deftype : deftype <: typeuse), x, i) = true
+  def $before{j : n, i : nat}(REC_typeuse(j), i) = (j < i)
   ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-  def $before{typeidx : typeidx, x : idx, i : nat}(_IDX_typeuse(typeidx), x, i) = (typeidx!`%`_typeidx.0 < x!`%`_idx.0)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-  def $before{j : n, x : idx, i : nat}(REC_typeuse(j), x, i) = (j < i)
+  def $before{typeuse : typeuse, i : nat}(typeuse, i) = true
+    -- otherwise
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
 def $unrollht(context : context, heaptype : heaptype) : subtype
@@ -2872,35 +2871,35 @@ relation Comptype_ok: `%|-%:OK`(context, comptype)
     -- Resulttype_ok: `%|-%:OK`(C, `%`_resulttype(t_2*{t_2 <- `t_2*`}))
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:98.1-98.126
-relation Subtype_ok2: `%|-%:%`(context, subtype, oktypeidxnat)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:169.1-177.49
-  rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, x : idx, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
-    `%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypeidxnat(x, i))
+relation Subtype_ok2: `%|-%:%`(context, subtype, oktypenat)
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:168.1-176.49
+  rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
+    `%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypenat(i))
     -- if (|typeuse*{typeuse <- `typeuse*`}| <= 1)
     -- (Typeuse_ok: `%|-%:OK`(C, typeuse))*{typeuse <- `typeuse*`}
-    -- (if $before(typeuse, x, i))*{typeuse <- `typeuse*`}
+    -- (if $before(typeuse, i))*{typeuse <- `typeuse*`}
     -- (if ($unrollht(C, (typeuse : typeuse <: heaptype)) = SUB_subtype(?(), typeuse'*{typeuse' <- `typeuse'*`}, comptype')))*{comptype' <- `comptype'*`, typeuse <- `typeuse*`, `typeuse'*` <- `typeuse'**`}
     -- Comptype_ok: `%|-%:OK`(C, comptype)
     -- (Comptype_sub: `%|-%<:%`(C, comptype, comptype'))*{comptype' <- `comptype'*`}
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:99.1-99.126
-relation Rectype_ok2: `%|-%:%`(context, rectype, oktypeidxnat)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:189.1-190.24
-  rule empty{C : context, x : idx, i : nat}:
-    `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidxnat(x, i))
+relation Rectype_ok2: `%|-%:%`(context, rectype, oktypenat)
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:188.1-189.23
+  rule empty{C : context, i : nat}:
+    `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypenat(i))
 
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:192.1-195.50
-  rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx, i : nat}:
-    `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, i))
-    -- Subtype_ok2: `%|-%:%`(C, subtype_1, OK_oktypeidxnat(x, i))
-    -- Rectype_ok2: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, (i + 1)))
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:191.1-194.49
+  rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, i : nat}:
+    `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypenat(i))
+    -- Subtype_ok2: `%|-%:%`(C, subtype_1, OK_oktypenat(i))
+    -- Rectype_ok2: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypenat((i + 1)))
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:100.1-100.102
 relation Deftype_ok: `%|-%:OK`(context, deftype)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:198.1-202.14
-  rule _{C : context, rectype : rectype, i : n, n : n, `subtype*` : subtype*, x : idx}:
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:197.1-201.14
+  rule _{C : context, rectype : rectype, i : n, n : n, `subtype*` : subtype*}:
     `%|-%:OK`(C, _DEF_deftype(rectype, i))
-    -- Rectype_ok2: `%|-%:%`({TYPES [], RECS subtype^n{subtype <- `subtype*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []} +++ C, rectype, OK_oktypeidxnat(x, 0))
+    -- Rectype_ok2: `%|-%:%`({TYPES [], RECS subtype^n{subtype <- `subtype*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []} +++ C, rectype, OK_oktypenat(0))
     -- if (rectype = REC_rectype(`%`_list(subtype^n{subtype <- `subtype*`})))
     -- if (i < n)
 
@@ -3141,11 +3140,11 @@ rec {
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:97.1-97.126
 relation Rectype_ok: `%|-%:%`(context, rectype, oktypeidx)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:180.1-181.23
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:179.1-180.23
   rule empty{C : context, x : idx}:
     `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidx(x))
 
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:183.1-186.48
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:182.1-185.48
   rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx}:
     `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidx(x))
     -- Subtype_ok: `%|-%:%`(C, subtype_1, OK_oktypeidx(x))
@@ -7655,7 +7654,7 @@ relation Context_ok: `|-%:OK`(context)
     -- if (C = {TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS jt*{jt <- `jt*`}, GLOBALS gt*{gt <- `gt*`}, MEMS mt*{mt <- `mt*`}, TABLES tt*{tt <- `tt*`}, FUNCS dt_F*{dt_F <- `dt_F*`}, DATAS ok*{ok <- `ok*`}, ELEMS et*{et <- `et*`}, LOCALS lct*{lct <- `lct*`}, LABELS [`%`_resulttype((rt : reftype <: valtype)*{rt <- `rt*`})], RETURN ?(`%`_resulttype(lift((rt' : reftype <: valtype)?{rt' <- `rt'?`}))), REFS x*{x <- `x*`}})
     -- if (C_0 = {TYPES dt^n{dt <- `dt*`}, RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []})
     -- (Deftype_ok: `%|-%:OK`({TYPES dt^n{dt <- `dt*`}[0 : i], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, dt))^(i<n){dt <- `dt*`}
-    -- (Subtype_ok2: `%|-%:%`({TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, st, OK_oktypeidxnat(`%`_typeidx(n), i)))^(i<m){st <- `st*`}
+    -- (Subtype_ok2: `%|-%:%`({TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, st, OK_oktypenat(i)))^(i<m){st <- `st*`}
     -- (Tagtype_ok: `%|-%:OK`(C_0, jt))*{jt <- `jt*`}
     -- (Globaltype_ok: `%|-%:OK`(C_0, gt))*{gt <- `gt*`}
     -- (Memtype_ok: `%|-%:OK`(C_0, mt))*{mt <- `mt*`}
@@ -14547,8 +14546,8 @@ relation Vectype_ok: `%|-%:OK`(context, vectype)
     `%|-%:OK`(C, vectype)
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-syntax oktypeidxnat =
-  | OK(typeidx : typeidx, nat)
+syntax oktypenat =
+  | OK(nat)
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
 relation Packtype_ok: `%|-%:OK`(context, packtype)
@@ -14582,13 +14581,12 @@ relation Vectype_sub: `%|-%<:%`(context, vectype, vectype)
     `%|-%<:%`(C, vectype, vectype)
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-def $before(typeuse : typeuse, typeidx : typeidx, nat : nat) : bool
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-  def $before{deftype : deftype, x : idx, i : nat}((deftype : deftype <: typeuse), x, i) = true
+def $before(typeuse : typeuse, nat : nat) : bool
   ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-  def $before{typeidx : typeidx, x : idx, i : nat}(_IDX_typeuse(typeidx), x, i) = (typeidx!`%`_typeidx.0 < x!`%`_idx.0)
+  def $before{j : n, i : nat}(REC_typeuse(j), i) = (j < i)
   ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-  def $before{j : n, x : idx, i : nat}(REC_typeuse(j), x, i) = (j < i)
+  def $before{typeuse : typeuse, i : nat}(typeuse, i) = true
+    -- otherwise
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
 def $unrollht(context : context, heaptype : heaptype) : subtype
@@ -14707,35 +14705,35 @@ relation Comptype_ok: `%|-%:OK`(context, comptype)
     -- Resulttype_ok: `%|-%:OK`(C, `%`_resulttype(t_2*{t_2 <- `t_2*`}))
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:98.1-98.126
-relation Subtype_ok2: `%|-%:%`(context, subtype, oktypeidxnat)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:169.1-177.49
-  rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, x : idx, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
-    `%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypeidxnat(x, i))
+relation Subtype_ok2: `%|-%:%`(context, subtype, oktypenat)
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:168.1-176.49
+  rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
+    `%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypenat(i))
     -- if (|typeuse*{typeuse <- `typeuse*`}| <= 1)
     -- (Typeuse_ok: `%|-%:OK`(C, typeuse))*{typeuse <- `typeuse*`}
-    -- (if $before(typeuse, x, i))*{typeuse <- `typeuse*`}
+    -- (if $before(typeuse, i))*{typeuse <- `typeuse*`}
     -- (if ($unrollht(C, (typeuse : typeuse <: heaptype)) = SUB_subtype(?(), typeuse'*{typeuse' <- `typeuse'*`}, comptype')))*{comptype' <- `comptype'*`, typeuse <- `typeuse*`, `typeuse'*` <- `typeuse'**`}
     -- Comptype_ok: `%|-%:OK`(C, comptype)
     -- (Comptype_sub: `%|-%<:%`(C, comptype, comptype'))*{comptype' <- `comptype'*`}
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:99.1-99.126
-relation Rectype_ok2: `%|-%:%`(context, rectype, oktypeidxnat)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:189.1-190.24
-  rule empty{C : context, x : idx, i : nat}:
-    `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidxnat(x, i))
+relation Rectype_ok2: `%|-%:%`(context, rectype, oktypenat)
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:188.1-189.23
+  rule empty{C : context, i : nat}:
+    `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypenat(i))
 
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:192.1-195.50
-  rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx, i : nat}:
-    `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, i))
-    -- Subtype_ok2: `%|-%:%`(C, subtype_1, OK_oktypeidxnat(x, i))
-    -- Rectype_ok2: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, (i + 1)))
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:191.1-194.49
+  rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, i : nat}:
+    `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypenat(i))
+    -- Subtype_ok2: `%|-%:%`(C, subtype_1, OK_oktypenat(i))
+    -- Rectype_ok2: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypenat((i + 1)))
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:100.1-100.102
 relation Deftype_ok: `%|-%:OK`(context, deftype)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:198.1-202.14
-  rule _{C : context, rectype : rectype, i : n, n : n, `subtype*` : subtype*, x : idx}:
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:197.1-201.14
+  rule _{C : context, rectype : rectype, i : n, n : n, `subtype*` : subtype*}:
     `%|-%:OK`(C, _DEF_deftype(rectype, i))
-    -- Rectype_ok2: `%|-%:%`({TYPES [], RECS subtype^n{subtype <- `subtype*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []} +++ C, rectype, OK_oktypeidxnat(x, 0))
+    -- Rectype_ok2: `%|-%:%`({TYPES [], RECS subtype^n{subtype <- `subtype*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []} +++ C, rectype, OK_oktypenat(0))
     -- if (rectype = REC_rectype(`%`_list(subtype^n{subtype <- `subtype*`})))
     -- if (i < n)
 
@@ -14976,11 +14974,11 @@ rec {
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:97.1-97.126
 relation Rectype_ok: `%|-%:%`(context, rectype, oktypeidx)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:180.1-181.23
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:179.1-180.23
   rule empty{C : context, x : idx}:
     `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidx(x))
 
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:183.1-186.48
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:182.1-185.48
   rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx}:
     `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidx(x))
     -- Subtype_ok: `%|-%:%`(C, subtype_1, OK_oktypeidx(x))
@@ -19492,7 +19490,7 @@ relation Context_ok: `|-%:OK`(context)
     -- if (C = {TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS jt*{jt <- `jt*`}, GLOBALS gt*{gt <- `gt*`}, MEMS mt*{mt <- `mt*`}, TABLES tt*{tt <- `tt*`}, FUNCS dt_F*{dt_F <- `dt_F*`}, DATAS ok*{ok <- `ok*`}, ELEMS et*{et <- `et*`}, LOCALS lct*{lct <- `lct*`}, LABELS [`%`_resulttype((rt : reftype <: valtype)*{rt <- `rt*`})], RETURN ?(`%`_resulttype(lift((rt' : reftype <: valtype)?{rt' <- `rt'?`}))), REFS x*{x <- `x*`}})
     -- if (C_0 = {TYPES dt^n{dt <- `dt*`}, RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []})
     -- (Deftype_ok: `%|-%:OK`({TYPES dt^n{dt <- `dt*`}[0 : i], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, dt))^(i<n){dt <- `dt*`}
-    -- (Subtype_ok2: `%|-%:%`({TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, st, OK_oktypeidxnat(`%`_typeidx(n), i)))^(i<m){st <- `st*`}
+    -- (Subtype_ok2: `%|-%:%`({TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, st, OK_oktypenat(i)))^(i<m){st <- `st*`}
     -- (Tagtype_ok: `%|-%:OK`(C_0, jt))*{jt <- `jt*`}
     -- (Globaltype_ok: `%|-%:OK`(C_0, gt))*{gt <- `gt*`}
     -- (Memtype_ok: `%|-%:OK`(C_0, mt))*{mt <- `mt*`}
@@ -26384,8 +26382,8 @@ relation Vectype_ok: `%|-%:OK`(context, vectype)
     `%|-%:OK`(C, vectype)
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-syntax oktypeidxnat =
-  | OK(typeidx : typeidx, nat)
+syntax oktypenat =
+  | OK(nat)
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
 relation Packtype_ok: `%|-%:OK`(context, packtype)
@@ -26419,13 +26417,12 @@ relation Vectype_sub: `%|-%<:%`(context, vectype, vectype)
     `%|-%<:%`(C, vectype, vectype)
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-def $before(typeuse : typeuse, typeidx : typeidx, nat : nat) : bool
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-  def $before{deftype : deftype, x : idx, i : nat}((deftype : deftype <: typeuse), x, i) = true
+def $before(typeuse : typeuse, nat : nat) : bool
   ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-  def $before{typeidx : typeidx, x : idx, i : nat}(_IDX_typeuse(typeidx), x, i) = (typeidx!`%`_typeidx.0 < x!`%`_idx.0)
+  def $before{j : n, i : nat}(REC_typeuse(j), i) = (j < i)
   ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
-  def $before{j : n, x : idx, i : nat}(REC_typeuse(j), x, i) = (j < i)
+  def $before{typeuse : typeuse, i : nat}(typeuse, i) = true
+    -- otherwise
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec
 def $unrollht(context : context, heaptype : heaptype) : subtype
@@ -26546,13 +26543,13 @@ relation Comptype_ok: `%|-%:OK`(context, comptype)
     -- Resulttype_ok: `%|-%:OK`(C, `%`_resulttype(t_2*{t_2 <- `t_2*`}))
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:98.1-98.126
-relation Subtype_ok2: `%|-%:%`(context, subtype, oktypeidxnat)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:169.1-177.49
-  rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, x : idx, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
-    `%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypeidxnat(x, i))
+relation Subtype_ok2: `%|-%:%`(context, subtype, oktypenat)
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:168.1-176.49
+  rule _{C : context, `typeuse*` : typeuse*, comptype : comptype, i : nat, `comptype'*` : comptype*, `typeuse'**` : typeuse**}:
+    `%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, comptype), OK_oktypenat(i))
     -- if (|typeuse*{typeuse <- `typeuse*`}| <= 1)
     -- (Typeuse_ok: `%|-%:OK`(C, typeuse))*{typeuse <- `typeuse*`}
-    -- (if $before(typeuse, x, i))*{typeuse <- `typeuse*`}
+    -- (if $before(typeuse, i))*{typeuse <- `typeuse*`}
     -- if (|`comptype'*`| = |`typeuse*`|)
     -- if (|`comptype'*`| = |`typeuse'**`|)
     -- (if ($unrollht(C, (typeuse : typeuse <: heaptype)) = SUB_subtype(?(), typeuse'*{typeuse' <- `typeuse'*`}, comptype')))*{comptype' <- `comptype'*`, typeuse <- `typeuse*`, `typeuse'*` <- `typeuse'**`}
@@ -26560,23 +26557,23 @@ relation Subtype_ok2: `%|-%:%`(context, subtype, oktypeidxnat)
     -- (Comptype_sub: `%|-%<:%`(C, comptype, comptype'))*{comptype' <- `comptype'*`}
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:99.1-99.126
-relation Rectype_ok2: `%|-%:%`(context, rectype, oktypeidxnat)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:189.1-190.24
-  rule empty{C : context, x : idx, i : nat}:
-    `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidxnat(x, i))
+relation Rectype_ok2: `%|-%:%`(context, rectype, oktypenat)
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:188.1-189.23
+  rule empty{C : context, i : nat}:
+    `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypenat(i))
 
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:192.1-195.50
-  rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx, i : nat}:
-    `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, i))
-    -- Subtype_ok2: `%|-%:%`(C, subtype_1, OK_oktypeidxnat(x, i))
-    -- Rectype_ok2: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, (i + 1)))
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:191.1-194.49
+  rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, i : nat}:
+    `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypenat(i))
+    -- Subtype_ok2: `%|-%:%`(C, subtype_1, OK_oktypenat(i))
+    -- Rectype_ok2: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypenat((i + 1)))
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:100.1-100.102
 relation Deftype_ok: `%|-%:OK`(context, deftype)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:198.1-202.14
-  rule _{C : context, rectype : rectype, i : n, n : n, `subtype*` : subtype*, x : idx}:
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:197.1-201.14
+  rule _{C : context, rectype : rectype, i : n, n : n, `subtype*` : subtype*}:
     `%|-%:OK`(C, _DEF_deftype(rectype, i))
-    -- Rectype_ok2: `%|-%:%`({TYPES [], RECS subtype^n{subtype <- `subtype*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []} +++ C, rectype, OK_oktypeidxnat(x, 0))
+    -- Rectype_ok2: `%|-%:%`({TYPES [], RECS subtype^n{subtype <- `subtype*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []} +++ C, rectype, OK_oktypenat(0))
     -- if (rectype = REC_rectype(`%`_list(subtype^n{subtype <- `subtype*`})))
     -- if (i < n)
 
@@ -26830,11 +26827,11 @@ rec {
 
 ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:97.1-97.126
 relation Rectype_ok: `%|-%:%`(context, rectype, oktypeidx)
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:180.1-181.23
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:179.1-180.23
   rule empty{C : context, x : idx}:
     `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidx(x))
 
-  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:183.1-186.48
+  ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:182.1-185.48
   rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx}:
     `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidx(x))
     -- Subtype_ok: `%|-%:%`(C, subtype_1, OK_oktypeidx(x))
@@ -31508,7 +31505,7 @@ relation Context_ok: `|-%:OK`(context)
     -- if (C = {TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS jt*{jt <- `jt*`}, GLOBALS gt*{gt <- `gt*`}, MEMS mt*{mt <- `mt*`}, TABLES tt*{tt <- `tt*`}, FUNCS dt_F*{dt_F <- `dt_F*`}, DATAS ok*{ok <- `ok*`}, ELEMS et*{et <- `et*`}, LOCALS lct*{lct <- `lct*`}, LABELS [`%`_resulttype((rt : reftype <: valtype)*{rt <- `rt*`})], RETURN ?(`%`_resulttype(lift((rt' : reftype <: valtype)?{rt' <- `rt'?`}))), REFS x*{x <- `x*`}})
     -- if (C_0 = {TYPES dt^n{dt <- `dt*`}, RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []})
     -- (Deftype_ok: `%|-%:OK`({TYPES dt^n{dt <- `dt*`}[0 : i], RECS [], TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, dt))^(i<n){dt <- `dt*`}
-    -- (Subtype_ok2: `%|-%:%`({TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, st, OK_oktypeidxnat(`%`_typeidx(n), i)))^(i<m){st <- `st*`}
+    -- (Subtype_ok2: `%|-%:%`({TYPES dt^n{dt <- `dt*`}, RECS st^m{st <- `st*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []}, st, OK_oktypenat(i)))^(i<m){st <- `st*`}
     -- (Tagtype_ok: `%|-%:OK`(C_0, jt))*{jt <- `jt*`}
     -- (Globaltype_ok: `%|-%:OK`(C_0, gt))*{gt <- `gt*`}
     -- (Memtype_ok: `%|-%:OK`(C_0, mt))*{mt <- `mt*`}
diff --git a/spectec/test-prose/doc/valid/types-in.rst b/spectec/test-prose/doc/valid/types-in.rst
index 08430a3ace..5953a606fd 100644
--- a/spectec/test-prose/doc/valid/types-in.rst
+++ b/spectec/test-prose/doc/valid/types-in.rst
@@ -95,11 +95,11 @@ Recursive Types
 $${definition: before}
 
 .. _syntax-oktypeidx:
-.. _syntax-oktypeidxnat:
+.. _syntax-oktypenat:
 
 $${syntax+:
   oktypeidx
-  oktypeidxnat
+  oktypenat
 }
 
 $${rule+:
diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md
index d666929f4e..40dd9dfab7 100644
--- a/spectec/test-splice/TEST.md
+++ b/spectec/test-splice/TEST.md
@@ -421,7 +421,7 @@ warning: syntax `num_` was never spliced
 warning: syntax `num_` was never spliced
 warning: syntax `numtype` was never spliced
 warning: syntax `oktypeidx` was never spliced
-warning: syntax `oktypeidxnat` was never spliced
+warning: syntax `oktypenat` was never spliced
 warning: syntax `pack_` was never spliced
 warning: syntax `packtype` was never spliced
 warning: syntax `packval` was never spliced