diff --git a/spectec/doc/semantics/il/1-syntax.spectec b/spectec/doc/semantics/il/1-syntax.spectec
index bb369461e0..07f4bafb55 100644
--- a/spectec/doc/semantics/il/1-syntax.spectec
+++ b/spectec/doc/semantics/il/1-syntax.spectec
@@ -130,6 +130,7 @@ syntax exp =
 
 syntax expfield = atom `= exp
 syntax exppull = id `: typ `<- exp
+syntax exppush = exp `-> id `: typ
 
 syntax path =
   | ROOT               ;;
@@ -174,8 +175,8 @@ syntax prem =
   | IF exp
   | ELSE
   | NOT prem
-  | LET exp `= exp  ;; TODO: variables/quantifiers?
-  | ITER prem iter exppull*
+  | LET `{quant*} exp `= exp
+  | ITER prem iter exppull* exppush*
 
 syntax dec =
   | TYP id param* `= inst*
diff --git a/spectec/doc/semantics/il/4-subst.spectec b/spectec/doc/semantics/il/4-subst.spectec
index 2b7f4f4176..ac134e2aa9 100644
--- a/spectec/doc/semantics/il/4-subst.spectec
+++ b/spectec/doc/semantics/il/4-subst.spectec
@@ -151,8 +151,12 @@ def $subst_prem(subst, prem) : prem
 def $subst_prem(s, REL x a* `: e) = REL x $subst_arg(s, a)* `: $subst_exp(s, e)
 def $subst_prem(s, IF e) = IF $subst_exp(s, e)
 def $subst_prem(s, ELSE) = ELSE
-def $subst_prem(s, LET e_1 `= e_2) = LET $subst_exp(s, e_1) `= $subst_exp(s, e_2)  ;; TODO: avoid capture
-def $subst_prem(s, ITER pr it (x `: t `<- e)*) = ITER $subst_prem(s, pr) $subst_iter(s, it) (x `: $subst_typ(s, t) `<- $subst_exp(s, e))*  ;; TODO: avoid capture
+def $subst_prem(s, LET `{q*} e_1 `= e_2) = LET `{$subst_param(s, q)*} $subst_exp(s, e_1) `= $subst_exp(s, e_2)  ;; TODO: avoid capture
+def $subst_prem(s, ITER pr it (x_1 `: t_1 `<- e_1)* (e_2 `-> x_2 `: t_2)*) =  ;; TODO: avoid capture
+  ITER $subst_prem(s, pr) $subst_iter(s, it) (x_1 `: $subst_typ(s, t_1) `<- $subst_exp(s, e_1))* ($subst_exp(s, e_2) `-> x_2 `: $subst_typ(s, t_2))*
+
+def $subst_exppush(subst, exppush) : exppush
+def $subst_exppush(s, e `-> x `: t) = $subst_exp(s, e) `-> x `: $subst_typ(s, t)
 
 
 def $subst_inst(subst, inst) : inst
diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec
index 91a55d66f8..9948e5003a 100644
--- a/spectec/doc/semantics/il/5-reduction.spectec
+++ b/spectec/doc/semantics/il/5-reduction.spectec
@@ -80,6 +80,7 @@ rule Step_typ/ITER-ctx:
 
 relation Step_iter: S |- iter ~> iter
 relation Step_exppull: S |- exppull ~> exppull
+relation Step_exppush: S |- exppush ~> exppush
 
 rule Step_iter/SUP-ctx:
   S |- SUP x e ~> SUP x e'
@@ -94,6 +95,14 @@ rule Step_exppull/ctx2:
   S |- x `: t `<- e  ~>  x `: t `<- e'
   -- Step_exp: S |- e ~> e'
 
+rule Step_exppush/ctx1:
+  S |- e `-> x `: t  ~>  e' `-> x `: t
+  -- Step_exp: S |- e ~> e'
+
+rule Step_exppush/ctx2:
+  S |- e `-> x `: t  ~>  e `-> x `: t'
+  -- Step_typ: S |- t ~> t'
+
 
 ;; Expressions
 
@@ -746,8 +755,8 @@ rule Step_clause/CLAUSE-ctx2:
   -- Step_exp: S |- e ~> e'
 
 rule Step_clause/CLAUSE-ctx3:
-  S |- CLAUSE `{q*} a* `= e `- pr* ~> CLAUSE `{q*} a* `= e `- pr'*
-  -- Step_prems: S |- pr* ~> pr'*
+  S |- CLAUSE `{q*} a* `= e `- pr* ~> CLAUSE `{q*} a* `= $subst_exp(s, e) `- pr'*
+  -- Step_prems: S |- pr* ~>_s pr'*
 
 
 ;; Arguments
@@ -785,7 +794,7 @@ rule Step_arg/TYP-ctx:
 ;; Premises
 
 relation Reduce_prems: S |- prem* ~>* prem*
-relation Step_prems: S |- prem* ~> prem*
+relation Step_prems: S |- prem* ~>_subst prem*
 relation Eq_prems: S |- prem* == prem*
 
 
@@ -801,74 +810,91 @@ rule Reduce_prems/refl:
 
 rule Reduce_prems/step:
   S |- pr* ~>* pr''*
-  -- Step_prems: S |- pr* ~> pr'*
+  -- Step_prems: S |- pr* ~>_s pr'*
   -- Reduce_prems: S |- pr'* ~>* pr''*
 
 
-rule Step_prems/ctx:
-  S |- pr* ~> pr*[0 : n] pr'_n* pr*[n : |pr*| - n]
-  -- Step_prems: S |- pr*[n] ~> pr'_n*
+rule Step_prems/seq:
+  S |- pr_1* pr pr_2* ~>_s pr_1* pr'* $subst_prem(s, pr_2)*
+  -- Step_prems: S |- pr ~>_s pr'*
 
 
 rule Step_prems/REL:
-  S |- REL x a* `: e ~> $subst_prem(s, pr)* (IF (CMP EQ $subst_exp(s, e') e))
+  S |- REL x a* `: e ~>_{} $subst_prem(s, pr)* (IF (CMP EQ $subst_exp(s, e') e))
   -- if (x, p* `-> t `= rul*) <- S.REL
   -- if (RULE `{q*} e' `- pr*) <- $subst_rule($args_for_params(a*, p*), rul)*
   -- Ok_subst: $storeenv(S) |- s : q*
   ;; Note: non-computational rule
 
 rule Step_prems/IF-ctx:
-  S |- IF e ~> IF e'
+  S |- IF e ~>_{} IF e'
   -- Step_exp: S |- e ~> e'
 
 rule Step_prems/IF-true:
-  S |- IF (BOOL true) ~> eps
+  S |- IF (BOOL true) ~>_{} eps
 
 rule Step_prems/ELSE:
-  S |- ELSE ~> IF (BOOL true)
+  S |- ELSE ~>_{} IF (BOOL true)
 
 rule Step_prems/LET-ctx:
-  S |- LET e_1 `= e_2 ~> LET e_1 `= e'_2
+  S |- LET `{q*} e_1 `= e_2 ~>_{} LET `{q*} e_1 `= e'_2
   -- Step_exp: S |- e_2 ~> e'_2
 
 rule Step_prems/LET:
-  S |- LET e `= e ~> eps
+  S |- LET `{(EXP x `: t)*} e_1 `= e_2 ~>_{EXP (x, e)*} eps
+  -- (if e = MATCH (EXP e_2) WITH (CLAUSE `{(EXP x `: t)*} (EXP e_1) `= (VAR x) `- eps))*
 
 rule Step_prems/NOT-ctx:
-  S |- NOT pr ~> NOT pr'
-  -- Step_prems: S |- pr ~> pr'
+  S |- NOT pr ~>_{} NOT pr'
+  -- Step_prems: S |- pr ~>_s pr'
 
 rule Step_prems/NOT-true:
-  S |- NOT (IF (BOOL true)) ~> IF (BOOL false)
+  S |- NOT (IF (BOOL true)) ~>_{} IF (BOOL false)
 
 rule Step_prems/NOT-false:
-  S |- NOT (IF (BOOL false)) ~> IF (BOOL true)
+  S |- NOT (IF (BOOL false)) ~>_{} IF (BOOL true)
+
+var ep : exppull
+var eq : exppush
 
 rule Step_prems/ITER-ctx1:
-  S |- ITER pr it ep* ~> ITER pr' it ep*
-  -- Step_prems: S |- pr ~> pr'
+  S |- ITER pr it ep* eq* ~>_{} ITER pr' it ep* $subst_exppush(s, eq)*
+  -- Step_prems: S |- pr ~>_s pr'
 
 rule Step_prems/ITER-ctx2:
-  S |- ITER pr it ep* ~> ITER pr it' ep*
+  S |- ITER pr it ep* eq* ~>_{} ITER pr it' ep* eq*
   -- Step_iter: S |- it ~> it'
 
 rule Step_prems/ITER-ctx3:
-  S |- ITER pr it ep* ~> ITER pr it ep*[[n] = ep'_n]
+  S |- ITER pr it ep* eq* ~>_{} ITER pr it ep*[[n] = ep'_n] eq*
   -- Step_exppull: S |- ep*[n] ~> ep'_n
 
+rule Step_prems/ITER-ctx4:
+  S |- ITER pr it ep* eq* ~>_{} ITER pr it ep* eq*[[n] = eq'_n]
+  -- Step_exppush: S |- eq*[n] ~> eq'_n
+
 rule Step_prems/ITER-QUEST:
-  S |- ITER pr QUEST (x `: t `<- OPT e?)* ~> $subst_prem({EXP (x, e')*}, pr)?
-  -- if e'*? = $transpose_(exp, e?*)
+  S |- ITER pr QUEST (x_1 `: t_1 `<- OPT e_1?)* (e_2 `-> x_2 `: t_2)* ~>_{EXP (x_2, OPT e''_2?)*}
+    $subst_prem({EXP (x_1, e'_1)*}, pr)?
+  -- if e'_1*? = $transpose_(exp, e_1?*)
+  -- if e'_2*? = $transpose_(exp, e''_2?*)
+  -- (if |e_1?| = |e''_2?|)*
+  -- (if e'_2 = e_2)*?
 
 rule Step_prems/ITER-PLUS:
-  S |- ITER pr PLUS (x `: t `<- LIST e*)* ~> ITER pr STAR (x `: t `<- LIST e*)*
-  -- if |e**[0]| >= 1
+  S |- ITER pr PLUS (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)* ~>_{}
+    ITER pr STAR (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)*
+  -- if |e_1**[0]| >= 1
 
 rule Step_prems/ITER-STAR:
-  S |- ITER pr STAR (x `: t `<- LIST e*)* ~> ITER pr (SUP y (NAT n)) (x `: t `<- LIST e*)*
-  -- if |e**[0]| = n
+  S |- ITER pr STAR (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)* ~>_{}
+    ITER pr (SUP y (NAT n)) (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)*
+  -- if |e_1**[0]| = n
   ;; TODO: y fresh
 
 rule Step_prems/ITER-SUP:
-  S |- ITER pr (SUP y (NAT n)) (x `: t `<- LIST e^n)* ~> $subst_prem({EXP (x, e')* (y, NAT i)}, pr)^(i<n)
-  -- if e'*^n = $transpose_(exp, e^n*)
+  S |- ITER pr (SUP y (NAT n)) (x_1 `: t_1 `<- LIST e_1^n)* ~>_{EXP (x_2, LIST e''_2^n)*}
+    $subst_prem({EXP (x_1, e'_1)* (y, NAT i)}, pr)^(i<n)
+  -- if e'_1*^n = $transpose_(exp, e_1^n*)
+  -- if e'_2*^n = $transpose_(exp, e''_2^n*)
+  -- (if e'_2 = e_2)*^n
diff --git a/spectec/doc/semantics/il/6-typing.spectec b/spectec/doc/semantics/il/6-typing.spectec
index 15ad528904..dc682c34ec 100644
--- a/spectec/doc/semantics/il/6-typing.spectec
+++ b/spectec/doc/semantics/il/6-typing.spectec
@@ -156,14 +156,14 @@ rule Ok_typfield:
   E |- (a `: t `- `{q*} pr*) : OK
   -- Ok_typ: E |- t : OK
   -- Ok_params: E ++ $tupenv(t) |- q* : OK
-  -- Ok_prems: E ++ $tupenv(t) ++ $paramenv(q*) |- pr* : OK
+  -- Ok_prems: E ++ $tupenv(t) ++ $paramenv(q*) |- pr* : OK -| E'
 
 
 rule Ok_typcase:
   E |- (m `: t `- `{q*} pr*) : OK
   -- Ok_typ: E |- t : OK
   -- Ok_params: E ++ $tupenv(t) |- q* : OK
-  -- Ok_prems: E ++ $tupenv(t) ++ $paramenv(q*) |- pr* : OK
+  -- Ok_prems: E ++ $tupenv(t) ++ $paramenv(q*) |- pr* : OK -| E'
 
 
 ;; Iterators
@@ -487,42 +487,50 @@ rule Ok_sym/conv:
 
 ;; Premises
 
-relation Ok_prem: E |- prem : OK
-relation Ok_prems: E |- prem* : OK
+relation Ok_prem: E |- prem : OK -| E
+relation Ok_prems: E |- prem* : OK -| E
+
+
+rule Ok_prems/eps:
+  E |- eps : OK -| {}
+
+rule Ok_prems/cons:
+  E |- pr_1 pr* : OK -| E_1 ++ E'
+  -- Ok_prem: E |- pr_1 : OK -| E_1
+  -- Ok_prems: E ++ E_1 |- pr* : OK -| E'
+
 
 rule Ok_prem/REL:
-  E |- REL x a* `: e : OK
+  E |- REL x a* `: e : OK -| {}
   -- if (x, (p* `-> t `= rul*)) <- E.REL
   -- Ok_args: E |- a* : p* => s
   -- Ok_exp: E |- e : $subst_typ(s, t)
 
 rule Ok_prem/IF:
-  E |- IF e : OK
+  E |- IF e : OK -| {}
   -- Ok_exp: E |- e : BOOL
 
 rule Ok_prem/ELSE:
-  E |- ELSE : OK
+  E |- ELSE : OK -| {}
 
 rule Ok_prem/NOT:
-  E |- NOT pr : OK
-  -- Ok_prem: E |- pr : OK
+  E |- NOT pr : OK -| {}
+  -- Ok_prem: E |- pr : OK -| {}
 
 rule Ok_prem/LET:
-  E |- LET e_1 `= e_2 : OK
-  -- Ok_exp: E |- e_1 : t
+  E |- LET `{q*} e_1 `= e_2 : OK -| $paramenv(q*)
+  -- Ok_exp: E ++ $paramenv(q*) |- e_1 : t
   -- Ok_exp: E |- e_2 : t
 
 rule Ok_prem/ITER:
-  E |- ITER pr it (x `: t `<- e)* : OK
+  E |- ITER pr it (x_1 `: t_1 `<- e_1)* (e_2 `-> x_2 `: t_2)* : OK -| {EXP (x_2, t_2)*}
   -- Ok_iter: E |- it : it' -| E'
-  -- (Ok_typ: E |- t : OK)*
-  -- (Ok_exp: E |- e : ITER t it')*
-  -- Ok_prem: E ++ {EXP (x, t)*} ++ E' |- pr : OK
-
-
-rule Ok_prems:
-  E |- prem* : OK
-  -- (Ok_prem: E |- prem : OK)*
+  -- (Ok_typ: E |- t_1 : OK)*
+  -- (Ok_exp: E |- e_1 : ITER t_1 it')*
+  -- Ok_prem: E ++ {EXP (x_1, t_1)*} ++ E' |- pr : OK -| E'
+  -- (Ok_typ: E |- t_2 : OK)*
+  -- (Eq_typ: E |- t_2 == ITER t'_2 it')*
+  -- (Ok_exp: E ++ E' |- e_2 : t'_2)*
 
 
 ;; Parameters and Arguments
@@ -644,7 +652,7 @@ rule Ok_rule:
   E |- RULE `{q*} e `- pr* : t
   -- Ok_params: E |- q* : OK
   -- Ok_exp: E ++ $paramenv(q*) |- e : t
-  -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK
+  -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK -| E'
 
 relation Ok_clause: E |- clause : param* -> typ
 
@@ -652,8 +660,8 @@ rule Ok_clause:
   E |- CLAUSE `{q*} a* `= e `- pr* : p* -> t
   -- Ok_params: E |- q* : OK
   -- Ok_args: E ++ $paramenv(q*) |- a* : p* => s
-  -- Ok_exp: E ++ $paramenv(q*) |- e : t
-  -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK
+  -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK -| E'
+  -- Ok_exp: E ++ $paramenv(q*) ++ E' |- e : t
 
 relation Ok_prod: E |- prod : typ
 
@@ -661,8 +669,8 @@ rule Ok_prod:
   E |- PROD `{q*} g `=> e `- pr* : t
   -- Ok_params: E |- q* : OK
   -- Ok_sym: E ++ $paramenv(q*) |- g : t'
-  -- Ok_exp: E ++ $paramenv(q*) |- e : t
-  -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK
+  -- Ok_prems: E ++ $paramenv(q*) |- pr* : OK -| E'
+  -- Ok_exp: E ++ $paramenv(q*) ++ E' |- e : t
 
 
 ;; Scripts