diff --git a/spectec/Makefile b/spectec/Makefile
index ed4ae2bb3c..c9935772e0 100644
--- a/spectec/Makefile
+++ b/spectec/Makefile
@@ -113,6 +113,12 @@ sync%:
 	(cd ../specification && make $@)
 
 
+# Semantics checks
+
+sem:
+	(cd doc/semantics/il && make check)
+
+
 # Cleanup
 
 .PHONY: clean distclean
diff --git a/spectec/doc/semantics/il/1-syntax.spectec b/spectec/doc/semantics/il/1-syntax.spectec
index 3fb61a8e09..6a006b24ad 100644
--- a/spectec/doc/semantics/il/1-syntax.spectec
+++ b/spectec/doc/semantics/il/1-syntax.spectec
@@ -31,8 +31,9 @@ syntax deftyp =
   | VARIANT typcase*
 
 syntax typbind = id `: typ
-syntax typfield = atom `: typ `- `{quant*} prem*
-syntax typcase = mixop `: typ `- `{quant*} prem*
+syntax typfield = atom `: typprems
+syntax typcase = mixop `: typprems
+syntax typprems = typ `- `{quant*} prem*
 
 
 ;; Iterators
@@ -130,6 +131,8 @@ syntax exp =
 
 syntax expfield = atom `= exp
 syntax exppull = id `: typ `<- exp
+syntax exppush = exp `-> id `: typ
+syntax expprems = exp `- prem*
 
 syntax path =
   | ROOT               ;;
@@ -174,8 +177,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*
@@ -185,9 +188,9 @@ syntax dec =
   | REC dec*
 
 syntax inst = INST `{quant*} arg* `=> deftyp
-syntax rul = RULE `{quant*} exp `- prem*
-syntax clause = CLAUSE `{quant*} arg* `=> exp `- prem*
-syntax prod = PROD `{quant*} sym `=> exp `- prem*
+syntax rul = RULE `{quant*} expprems
+syntax clause = CLAUSE `{quant*} arg* `=> expprems
+syntax prod = PROD `{quant*} sym `=> expprems
 
 
 ;; Scripts
diff --git a/spectec/doc/semantics/il/4-subst.spectec b/spectec/doc/semantics/il/4-subst.spectec
index 3e90548cc7..1e10ba0248 100644
--- a/spectec/doc/semantics/il/4-subst.spectec
+++ b/spectec/doc/semantics/il/4-subst.spectec
@@ -107,12 +107,38 @@ def $refresh_exppulls(ep*) = (ep', $composesubsts(s*))
   -- (if (ep', s) = $refresh_exppull(ep))*
 
 
+def $refresh_exppush(exppush) : (exppush, subst)
+def $refresh_exppushs(exppush*) : (exppush*, subst)
+
+def $refresh_exppush(e `-> x `: t) = (e `-> x' `: t, s)
+  -- if (x', s) = $refresh_expid(x)
+
+def $refresh_exppushs(eq*) = (eq', $composesubsts(s*))
+  -- (if (eq', s) = $refresh_exppush(eq))*
+
+
 def $refresh_iter(iter) : (iter, subst)
 
 def $refresh_iter(QUEST) = (QUEST, {})
 def $refresh_iter(STAR) = (STAR, {})
 def $refresh_iter(PLUS) = (PLUS, {})
-def $refresh_iter(SUP x e) = (SUP x' e, s) -- if (x', s) = $refresh_expid(x)
+def $refresh_iter(SUP x e) = (SUP x' e, s)
+  -- if (x', s) = $refresh_expid(x)
+
+
+def $refresh_prem(prem) : (prem, subst)
+def $refresh_prems(prem*) : (prem*, subst)
+
+def $refresh_prem(REL x a* `: e) = (REL x a* `: e, {})
+def $refresh_prem(IF e) = (IF e, {})
+def $refresh_prem(ELSE) = (ELSE, {})
+def $refresh_prem(LET `{q*} e_1 `= e_2) = (LET `{q'*} $subst_exp(s, e_1) `= e_2, s)
+  -- if (q'*, s) = $refresh_params(q*)
+def $refresh_prem(ITER pr it ep* eq*) = (ITER pr it ep* eq'*, s)
+  -- if (eq'*, s) = $refresh_exppushs(eq*)
+
+def $refresh_prems(pr*) =
+  $refresh_list(prem, $refresh_prem, $subst_prem, pr*)
 
 
 ;; Lists
@@ -142,12 +168,8 @@ def $subst_typ(s, MATCH x a* WITH inst*) = MATCH x $subst_arg(s, a)*  WITH $subs
 
 def $subst_deftyp(subst, deftyp) : deftyp
 def $subst_deftyp(s, ALIAS t) = ALIAS $subst_typ(s, t)
-def $subst_deftyp(s, STRUCT (a `: t `- `{q*} pr*)*) = STRUCT (a `: $subst_typ(s, t') `- `{$subst_param(s ++ s', q')*} $subst_prem(s ++ s' ++ s'', pr)*)*
-  -- if (t', s') = $refresh_typ(t)
-  -- if (q'*, s'') = $refresh_params(q*)
-def $subst_deftyp(s, VARIANT (m `: t `- `{q*} pr*)*) = VARIANT (m `: $subst_typ(s, t') `- `{$subst_param(s ++ s', q')*} $subst_prem(s ++ s' ++ s'', pr)*)*
-  -- if (t', s') = $refresh_typ(t)
-  -- if (q'*, s'') = $refresh_params(q*)
+def $subst_deftyp(s, STRUCT (a `: tpr)*) = STRUCT (a `: $subst_typprems(s, tpr))*
+def $subst_deftyp(s, VARIANT (m `: tpr)*) = VARIANT (m `: $subst_typprems(s, tpr))*
 
 def $subst_typbind(subst, typbind) : typbind
 def $subst_typbind(s, x `: t) = x' `: $subst_typ(s, t)
@@ -164,6 +186,9 @@ def $subst_iter(s, SUP x e) = SUP x $subst_exp(s, e)
 def $subst_exppull(subst, exppull) : exppull
 def $subst_exppull(s, x `: t `<- e') = x `: $subst_typ(s, t) `<- $subst_exp(s, e')
 
+def $subst_exppush(subst, exppush) : exppush
+def $subst_exppush(s, e' `-> x `: t) = $subst_exp(s, e') `-> x `: $subst_typ(s, t)
+
 
 ;; Expressions
 
@@ -223,7 +248,7 @@ def $subst_sym(s, ITER g it ep*) = ITER $subst_sym(s ++ s' ++ s'', g) $subst_ite
   -- if (ep'*, s'') = $refresh_exppulls(ep*)
 
 
-;; Definitions
+;; Arguments and Parameters
 
 def $subst_arg(subst, arg) : arg
 def $subst_arg(s, TYP t) = TYP $subst_typ(s, t)
@@ -239,30 +264,49 @@ def $subst_param(s, FUN x `: p* `-> t) = FUN x `: $subst_param(s, p')* `-> $subs
 def $subst_param(s, GRAM x `: p* `-> t) = GRAM x `: $subst_param(s, p')* `-> $subst_typ(s ++ s', t)
   -- if (p'*, s') = $refresh_params(p*)
 
+
+;; Premises
+
 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)
-def $subst_prem(s, ITER pr it ep*) = ITER $subst_prem(s ++ s' ++ s'', pr) $subst_iter(s, it') $subst_exppull(s, ep')*
+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)
+  ;; Assume: q* fresh (from caller $subst_typprems, $subst_expprems)
+def $subst_prem(s, ITER pr it ep* eq*) = ITER $subst_prem(s ++ s' ++ s'', pr') $subst_iter(s, it') $subst_exppull(s, ep')* $subst_exppush(s ++ s''', eq')*
+  ;; Assume: eq* fresh (from caller $subst_typprems, $subst_expprems)
   -- if (it', s') = $refresh_iter(it)
   -- if (ep'*, s'') = $refresh_exppulls(ep*)
+  -- if (pr', s''') = $refresh_prem(pr)
+
 
+def $subst_typprems(subst, typprems) : typprems
+def $subst_typprems(s, t `- `{q*} pr*) = $subst_typ(s, t') `- `{$subst_param(s ++ s', q')*} $subst_prem(s ++ s' ++ s'', pr')*
+  -- if (t', s') = $refresh_typ(t)
+  -- if (q'*, s'') = $refresh_params(q*)
+  -- if (pr'*, s''') = $refresh_prems(pr*)
+
+def $subst_expprems(subst, expprems) : expprems
+def $subst_expprems(s, e `- pr*) = $subst_exp(s ++ s', e) `- $subst_prem(s, pr)*
+  -- if (pr'*, s') = $refresh_prems(pr*)
+
+
+;; Definitions
 
 def $subst_inst(subst, inst) : inst
 def $subst_inst(s, INST `{q*} a* `=> dt) = INST `{$subst_param(s, q')*} $subst_arg(s ++ s', a)* `=> $subst_deftyp(s ++ s', dt)
   -- if (q'*, s') = $refresh_params(q*)
 
 def $subst_rule(subst, rul) : rul
-def $subst_rule(s, RULE `{q*} e `- pr*) = RULE `{$subst_param(s, q')*} $subst_exp(s ++ s', e) `- $subst_prem(s ++ s', pr)*
+def $subst_rule(s, RULE `{q*} epr) = RULE `{$subst_param(s, q')*} $subst_expprems(s ++ s', epr)
   -- if (q'*, s') = $refresh_params(q*)
 
 def $subst_clause(subst, clause) : clause
-def $subst_clause(s, CLAUSE `{q*} a* `=> e `- pr*) = CLAUSE `{$subst_param(s, q')*} $subst_arg(s ++ s', a)* `=> $subst_exp(s ++ s', e) `- $subst_prem(s ++ s', pr)*
+def $subst_clause(s, CLAUSE `{q*} a* `=> epr) = CLAUSE `{$subst_param(s, q')*} $subst_arg(s ++ s', a)* `=> $subst_expprems(s ++ s', epr)
   -- if (q'*, s') = $refresh_params(q*)
 
 def $subst_prod(subst, prod) : prod
-def $subst_prod(s, PROD `{q*} g `=> e `- pr*) = PROD `{$subst_param(s, q')*} $subst_sym(s ++ s', g) `=> $subst_exp(s ++ s', e) `- $subst_prem(s ++ s', pr)*
+def $subst_prod(s, PROD `{q*} g `=> epr) = PROD `{$subst_param(s, q')*} $subst_sym(s ++ s', g) `=> $subst_expprems(s ++ s', epr)
   -- if (q'*, s') = $refresh_params(q*)
 
 
diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec
index 72ee64a5fa..a8c699a3c9 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
 
@@ -442,9 +451,9 @@ rule Step_exp/MATCH-ctx2:
   -- Step_clause: S |- clause*[n] ~> clause'_n
 
 rule Step_exp/MATCH-match:
-  S |- MATCH a* WITH (CLAUSE `{q*} a'* `=> e `- pr*) clause* ~>
+  S |- MATCH a* WITH (CLAUSE `{q*} a'* `=> epr) clause* ~>
     MATCH a''* WITH
-      (CLAUSE `{q'*} a'''* `=> $subst_exp(s, e) `- $subst_prem(s, pr)*)
+      (CLAUSE `{q'*} a'''* `=> $subst_expprems(s, epr))
       (CLAUSE `{} a''* `=> (MATCH a* WITH clause*) `- eps)
   -- Step_argmatch: S |- `{q*} (a / a')*  ~>_s  `{q'*} (a'' / a''')*
 
@@ -695,6 +704,7 @@ rule Step_expmatch_plain/STR-fail:
   S |- STR ef* / STR ef'* ~> FAIL
   -- otherwise
 
+
 rule Step_expmatch_plain/ITER-PLUS:
   S |- LIST e* / ITER e' PLUS (x `: t `<- e_p)* ~>
     LIST e* / ITER e' STAR (x `: t `<- e_p)*
@@ -743,8 +753,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
@@ -782,7 +792,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*
 
 
@@ -798,74 +808,96 @@ 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 ++ s') pr_1* pr'* $subst_prem(s, pr'_2)*
+  -- Step_prems: S |- pr ~>_s pr'*
+  -- if (pr'_2*, s') = $refresh_prems(pr_2*)
 
 
 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 ~>_{} pr'* (IF (CMP EQ $subst_exp(s ++ s', e') e))
   -- if (x, p* `-> t `= rul*) <- S.REL
-  -- if (RULE `{q*} e' `- pr*) <- $subst_rule($args_for_params(a*, p*), rul)*
+  -- if (RULE `{q*} (e' `- pr*)) <- $subst_rule($args_for_params(a*, p*), rul)*
   -- Ok_subst: $storeenv(S) |- s : q*
+  -- if (pr'*, s') = $refresh_prems(pr*)
   ;; 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))*
+  ;; TODO: Propagate false in case of match failure
 
 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 $subst_exp(s', e''_2)?)*} ++ s')
+    $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)*?
+  -- if (pr', s') = $refresh_prem(pr)
 
 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
   -- Fresh_id: 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 $subst_exp(s', e''_2)^n)*} ++ s')
+    $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
+  -- if (pr', s') = $refresh_prem(pr)
diff --git a/spectec/doc/semantics/il/6-typing.spectec b/spectec/doc/semantics/il/6-typing.spectec
index e3c9ed0ee3..ddb982abaf 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
diff --git a/spectec/doc/semantics/il/Makefile b/spectec/doc/semantics/il/Makefile
new file mode 100644
index 0000000000..f97906fd16
--- /dev/null
+++ b/spectec/doc/semantics/il/Makefile
@@ -0,0 +1,4 @@
+SPECTEC = ../../../spectec
+
+check:
+	$(SPECTEC) *.spectec
diff --git a/spectec/src/backend-ast/print.ml b/spectec/src/backend-ast/print.ml
index 1372e94ea3..47696cfd02 100644
--- a/spectec/src/backend-ast/print.ml
+++ b/spectec/src/backend-ast/print.ml
@@ -162,7 +162,7 @@ and prem pr =
   match pr.it with
   | RulePr (x, as1, op, e) -> Node ("rule", id x :: List.map arg as1 @ [mixop op; exp e])
   | IfPr e -> Node ("if", [exp e])
-  | LetPr (e1, e2, _xs) -> Node ("let", [exp e1; exp e2])
+  | LetPr (_qs, e1, e2) -> Node ("let", [exp e1; exp e2])
   | ElsePr -> Atom "else"
   | IterPr (pr1, it) -> Node ("iter", [prem pr1] @ iterexp it)
 
diff --git a/spectec/src/backend-prose/gen.ml b/spectec/src/backend-prose/gen.ml
index 29e8389a7c..f84db74fd7 100644
--- a/spectec/src/backend-prose/gen.ml
+++ b/spectec/src/backend-prose/gen.ml
@@ -276,7 +276,7 @@ let inject_ctx frees c stmts =
 
 let rec prem_to_instrs prem =
   match prem.it with
-  | Ast.LetPr (e1, e2, _) ->
+  | Ast.LetPr (_, e1, e2) ->
     [ LetS (exp_to_expr e1, exp_to_expr e2) ]
   | Ast.IfPr e ->
     if_expr_to_instrs e
diff --git a/spectec/src/frontend/det.ml b/spectec/src/frontend/det.ml
index 840479ea31..f5ae1da69a 100644
--- a/spectec/src/frontend/det.ml
+++ b/spectec/src/frontend/det.ml
@@ -188,7 +188,7 @@ and det_prem pr =
   match pr.it with
   | RulePr (_x, _as, _mixop, e) -> det_exp e
   | IfPr e -> det_cond_exp e
-  | LetPr (e1, _e2, _xs) -> det_exp e1
+  | LetPr (_qs, e1, _e2) -> det_exp e1
   | ElsePr -> empty
   | IterPr (pr1, ite) -> det_iterexp (det_prem pr1) ite
 
diff --git a/spectec/src/frontend/dim.ml b/spectec/src/frontend/dim.ml
index 6e733fdb7e..f100989949 100644
--- a/spectec/src/frontend/dim.ml
+++ b/spectec/src/frontend/dim.ml
@@ -260,7 +260,8 @@ and check_prem dims ctx prem =
     check_exp dims ctx e
   | IfPr e -> check_exp dims ctx e
   | ElsePr -> ()
-  | LetPr (e1, e2, _xs) ->
+  | LetPr (qs, e1, e2) ->
+    List.iter (check_param dims) qs;
     check_exp dims ctx e1;
     check_exp dims ctx e2
   | IterPr (prem1, ite) ->
@@ -678,10 +679,11 @@ and annot_prem dims prem : prem * occur =
     | IfPr e ->
       let e', occur = annot_exp `Rhs dims e in
       IfPr e', occur
-    | LetPr (e1, e2, ids) ->
+    | LetPr (qs, e1, e2) ->
+      let qs', occurs = List.split (List.map (annot_param dims) qs) in
       let e1', occur1 = annot_exp `Lhs dims e1 in
       let e2', occur2 = annot_exp `Rhs dims e2 in
-      LetPr (e1', e2', ids), union occur1 occur2
+      LetPr (qs', e1', e2'), List.fold_left union (union occur1 occur2) occurs
     | ElsePr ->
       ElsePr, Map.empty
     | IterPr (prem1, iter) ->
diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml
index 7cb5709e5c..c1f545019f 100644
--- a/spectec/src/il/ast.ml
+++ b/spectec/src/il/ast.ml
@@ -156,7 +156,7 @@ and prem = prem' phrase
 and prem' =
   | RulePr of id * arg list * mixop * exp             (* premise *)
   | IfPr of exp                                       (* side condition *)
-  | LetPr of exp * exp * string list                  (* binding *)
+  | LetPr of quant list * exp * exp                   (* binding *)
   | ElsePr                                            (* otherwise *)
   | IterPr of prem * iterexp                          (* iteration *)
 
diff --git a/spectec/src/il/eq.ml b/spectec/src/il/eq.ml
index a814f50efa..804fb9d7ba 100644
--- a/spectec/src/il/eq.ml
+++ b/spectec/src/il/eq.ml
@@ -147,8 +147,8 @@ and eq_prem prem1 prem2 =
   | IfPr e1, IfPr e2 -> eq_exp e1 e2
   | IterPr (prem1, e1), IterPr (prem2, e2) ->
     eq_prem prem1 prem2 && eq_iterexp e1 e2
-  | LetPr (e1, e1', xs1), LetPr (e2, e2', xs2) ->
-    eq_exp e1 e2 && eq_exp e1' e2' && xs1 = xs2
+  | LetPr (qs1, e11, e12), LetPr (qs2, e21, e22) ->
+    eq_list eq_param qs1 qs2 && eq_exp e11 e21 && eq_exp e12 e22
   | _, _ -> prem1.it = prem2.it
 
 
diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml
index 8c9679a5bb..d7bbb6ccd7 100644
--- a/spectec/src/il/eval.ml
+++ b/spectec/src/il/eval.ml
@@ -498,7 +498,7 @@ and reduce_prem env prem : [`True of Subst.t | `False | `None] =
     | _ -> `None
     )
   | ElsePr -> `True Subst.empty
-  | LetPr (e1, e2, _ids) ->
+  | LetPr (_qs, e1, e2) ->
     (match match_exp env Subst.empty e2 e1 with
     | Some s -> `True s
     | None -> `None
@@ -510,7 +510,7 @@ and reduce_prem env prem : [`True of Subst.t | `False | `None] =
      * and others, which are assumed to flow inwards. *)
     let rec is_let_bound prem (x, _) =
       match prem.it with
-      | LetPr (_, _, xs) -> List.mem x.it xs
+      | LetPr (qs, _, _) -> Free.(Set.mem x.it (bound_quants qs).varid)
       | IterPr (premI, iterexpI) ->
         let _iter1', xes1' = reduce_iterexp env iterexpI in
         let xes1_out, _ = List.partition (is_let_bound premI) xes1' in
@@ -961,7 +961,7 @@ and equiv_prem env pr1 pr2 =
   | RulePr (id1, mixop1, e1), RulePr (id2, mixop2, e2) ->
     id1.it = id2.it && Eq.eq_mixop mixop1 mixop2 && equiv_exp env e1 e2
   | IfPr e1, IfPr e2 -> equiv_exp env e1 e2
-  | LetPr (e11, e12, _ids1), LetPr (e21, e22, _id2) ->
+  | LetPr (_qs1, e11, e12), LetPr (_qs2, e21, e22) ->
     equiv_exp env e11 e21 && equiv_exp env e12 e22
   | IterPr (pr11, iter1), IterPr (pr21, iter2) ->
     equiv_prem env pr11 pr21 && equiv_iter env (fst iter1) (fst iter2)
diff --git a/spectec/src/il/free.ml b/spectec/src/il/free.ml
index 728810da51..71c54bb204 100644
--- a/spectec/src/il/free.ml
+++ b/spectec/src/il/free.ml
@@ -110,11 +110,16 @@ and free_prem prem =
   match prem.it with
   | RulePr (x, as_, _op, e) -> free_relid x ++ free_args as_ ++ free_exp e
   | IfPr e -> free_exp e
-  | LetPr (e1, e2, _) -> free_exp e1 ++ free_exp e2
+  | LetPr (qs, e1, e2) -> (free_exp e1 -- bound_quants qs) ++ free_exp e2
   | ElsePr -> empty
   | IterPr (prem1, ite) -> (free_prem prem1 -- bound_iterexp ite) ++ free_iterexp ite
 
-and free_prems prems = free_list free_prem prems
+and bound_prem prem =
+  match prem.it with
+  | LetPr (qs, _e1, _e2) -> bound_quants qs
+  | _ -> empty
+
+and free_prems prems = free_list_dep free_prem bound_prem prems
 
 
 (* Definitions *)
diff --git a/spectec/src/il/free.mli b/spectec/src/il/free.mli
index 1b962475c4..2744ccf838 100644
--- a/spectec/src/il/free.mli
+++ b/spectec/src/il/free.mli
@@ -24,6 +24,7 @@ val free_params : param list -> sets
 
 val bound_iter : iter -> sets
 val bound_iterexp : iterexp -> sets
+val bound_prem : prem -> sets
 val bound_quant : quant -> sets
 val bound_param : param -> sets
 val bound_def : def -> sets
diff --git a/spectec/src/il/iter.ml b/spectec/src/il/iter.ml
index 3688a48458..7b194b3d63 100644
--- a/spectec/src/il/iter.ml
+++ b/spectec/src/il/iter.ml
@@ -210,7 +210,7 @@ and prem pr =
   | IfPr e -> exp e
   | ElsePr -> ()
   | IterPr (pr1, it) -> iterexp prem pr1 it
-  | LetPr (e1, e2, _) -> exp e1; exp e2
+  | LetPr (qs, e1, e2) -> params qs; exp e1; exp e2
 
 and prems prs = list prem prs
 
@@ -244,19 +244,19 @@ let hintdef d =
 
 let inst i =
   match i.it with
-  | InstD (ps, as_, dt) -> params ps; args as_; deftyp dt
+  | InstD (qs, as_, dt) -> params qs; args as_; deftyp dt
 
 let rule r =
   match r.it with
-  | RuleD (x, ps, op, e, prs) -> ruleid x; params ps; mixop op; exp e; prems prs
+  | RuleD (x, qs, op, e, prs) -> ruleid x; params qs; mixop op; exp e; prems prs
 
 let clause c =
   match c.it with
-  | DefD (ps, as_, e, prs) -> params ps; args as_; exp e; prems prs
+  | DefD (qs, as_, e, prs) -> params qs; args as_; exp e; prems prs
 
 let prod p =
   match p.it with
-  | ProdD (ps, g, e, prs) -> params ps; sym g; exp e; prems prs
+  | ProdD (qs, g, e, prs) -> params qs; sym g; exp e; prems prs
 
 let rec def d =
   visit_def d;
diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml
index 05aea3ef35..110322ced9 100644
--- a/spectec/src/il/print.ml
+++ b/spectec/src/il/print.ml
@@ -218,10 +218,9 @@ and string_of_prem prem =
     string_of_id x ^ string_of_args as1 ^ ": " ^
     string_of_mixop mixop ^ string_of_exp_args e
   | IfPr e -> "if " ^ string_of_exp e
-  | LetPr (e1, e2, xs) ->
-    let xs' = List.map (fun x -> x $ no_region) xs in
-    "where " ^ string_of_exp e1 ^ " = " ^ string_of_exp e2 ^
-    " {" ^ (String.concat ", " (List.map string_of_id xs')) ^ "}"
+  | LetPr (qs, e1, e2) ->
+    "let" ^ string_of_quants qs ^ " " ^
+    string_of_exp e1 ^ " = " ^ string_of_exp e2
   | ElsePr -> "otherwise"
   | IterPr ({it = IterPr _; _} as prem', iter) ->
     string_of_prem prem' ^ string_of_iterexp iter
diff --git a/spectec/src/il/subst.ml b/spectec/src/il/subst.ml
index 885ed05e40..d73b4ecd3a 100644
--- a/spectec/src/il/subst.ml
+++ b/spectec/src/il/subst.ml
@@ -141,12 +141,12 @@ and subst_deftyp s dt =
 and subst_typfield s (atom, (t, qs, prems), hints) =
   let t', s' = subst_typ' s t in
   let qs', s'' = subst_quants s' qs in
-  (atom, (t', qs', subst_list subst_prem s'' prems), hints)
+  (atom, (t', qs', subst_prems s'' prems), hints)
 
 and subst_typcase s (op, (t, qs, prems), hints) =
   let t', s' = subst_typ' s t in
   let qs', s'' = subst_quants s' qs in
-  (op, (t', qs', subst_list subst_prem s'' prems), hints)
+  (op, (t', qs', subst_prems s'' prems), hints)
 
 
 (* Expressions *)
@@ -237,9 +237,14 @@ and subst_prem s prem =
   | IterPr (prem1, iterexp) ->
     let prem1', it' = subst_iterexp s subst_prem prem1 iterexp in
     IterPr (prem1', it')
-  | LetPr (e1, e2, xs) -> LetPr (subst_exp s e1, subst_exp s e2, xs)
+  | LetPr (qs, e1, e2) ->
+    let s' = remove_varids s (Free.bound_quants qs).Free.varid in
+    LetPr (qs, subst_exp s' e1, subst_exp s e2)
   ) $ prem.at
 
+and subst_prems s prems =
+  fst (subst_list_dep subst_prem Free.bound_prem s prems)
+
 
 (* Definitions *)
 
@@ -274,4 +279,4 @@ let subst_typ s t = if s = empty then t else subst_typ s t
 let subst_deftyp s dt = if s = empty then dt else subst_deftyp s dt
 let subst_exp s e = if s = empty then e else subst_exp s e
 let subst_sym s g = if s = empty then g else subst_sym s g
-let subst_prem s pr = if s = empty then pr else subst_prem s pr
+let subst_prems s prs = if s = empty then prs else subst_prems s prs
diff --git a/spectec/src/il/subst.mli b/spectec/src/il/subst.mli
index c8fd8fc5d8..5d28899999 100644
--- a/spectec/src/il/subst.mli
+++ b/spectec/src/il/subst.mli
@@ -39,6 +39,7 @@ val subst_deftyp : subst -> deftyp -> deftyp
 val subst_typcase : subst -> typcase -> typcase
 val subst_typfield : subst -> typfield -> typfield
 
+val subst_prems : subst -> prem list -> prem list
 val subst_args : subst -> arg list -> arg list
 val subst_params : subst -> param list -> param list * subst
 
diff --git a/spectec/src/il/valid.ml b/spectec/src/il/valid.ml
index 7a0fe7eb65..526858689d 100644
--- a/spectec/src/il/valid.ml
+++ b/spectec/src/il/valid.ml
@@ -249,7 +249,7 @@ and valid_typfield env (atom, (t, qs, prems), _hints) =
   valid_atom env atom;
   let env' = valid_typ_bind env t in
   let env'' = valid_quants env' qs in
-  List.iter (valid_prem env'') prems
+  ignore (valid_prems env'' prems)
 
 and valid_typcase env (mixop, (t, qs, prems), _hints) =
   Debug.(log_at "il.valid_typcase" t.at
@@ -267,7 +267,7 @@ and valid_typcase env (mixop, (t, qs, prems), _hints) =
   valid_mixop env mixop;
   let env' = valid_typ_bind env t in
   let env'' = valid_quants env' qs in
-  List.iter (valid_prem env'') prems
+  ignore (valid_prems env'' prems)
 
 
 (* Expressions *)
@@ -592,26 +592,33 @@ and valid_prem env prem =
     let ps, mixop', t, _rules = Env.find_rel env x in
     assert (Mixop.eq mixop mixop');
     let s = valid_args env as_ ps Subst.empty prem.at in
-    valid_expmix env mixop e (mixop, Subst.subst_typ s t) e.at
+    valid_expmix env mixop e (mixop, Subst.subst_typ s t) e.at;
+    env
   | IfPr e ->
-    valid_exp env e (BoolT $ e.at)
-  | LetPr (e1, e2, xs) ->
+    valid_exp env e (BoolT $ e.at);
+    env
+  | LetPr (qs, e1, e2) ->
+    let env' = valid_quants env qs in
     let t = infer_exp env e2 in
-    valid_exp ~side:`Lhs env e1 t;
+    valid_exp ~side:`Lhs env' e1 t;
     valid_exp env e2 t;
-    let target_ids = Free.{empty with varid = Set.of_list xs} in
-    let free_ids = Free.(free_exp e1) in
-    if not (Free.subset target_ids free_ids) then
-      error prem.at ("target identifier(s) " ^
-        ( Free.Set.elements (Free.diff target_ids free_ids).varid |>
+    let bound = Free.(bound_quants qs) in
+    let free = Free.(free_exp e1) in
+    if not (Free.subset bound free) then
+      error prem.at ("quantified identifier(s) " ^
+        ( Free.Set.elements (Free.diff bound free).varid |>
           List.map (fun x -> "`" ^ x ^ "`") |>
           String.concat ", " ) ^
-        " do not occur in left-hand side expression")
+        " do not occur in left-hand side expression");
+    env'
   | ElsePr ->
-    ()
+    env
   | IterPr (prem', ite) ->
     let _it, env' = valid_iterexp env ite prem.at in
-    valid_prem env' prem'
+    let _env'' = valid_prem env' prem' in
+    env  (* TODO: out it *)
+
+and valid_prems env prems = List.fold_left valid_prem env prems
 
 
 (* Definitions *)
@@ -695,7 +702,7 @@ let valid_rule env mixop t rule =
   | RuleD (_x, qs, mixop', e, prems) ->
     let env' = valid_quants env qs in
     valid_expmix ~side:`Lhs env' mixop' e (mixop, t) e.at;
-    List.iter (valid_prem env') prems
+    ignore (valid_prems env' prems)
 
 let valid_clause env x ps t clause =
   Debug.(log_in "il.valid_clause" line);
@@ -706,8 +713,8 @@ let valid_clause env x ps t clause =
   | DefD (qs, as_, e, prems) ->
     let env' = valid_quants env qs in
     let s = valid_args env' as_ ps Subst.empty clause.at in
-    valid_exp env' e (Subst.subst_typ s t);
-    List.iter (valid_prem env') prems
+    let env'' = valid_prems env' prems in
+    valid_exp env'' e (Subst.subst_typ s t)
 
 let valid_prod env ps t prod =
   Debug.(log_in "il.valid_prod" line);
@@ -718,8 +725,8 @@ let valid_prod env ps t prod =
   | ProdD (qs, g, e, prems) ->
     let env' = valid_quants env qs in
     let _t' = valid_sym env' g in
-    valid_exp env' e t;
-    List.iter (valid_prem env') prems
+    let env'' = valid_prems env' prems in
+    valid_exp env'' e t
 
 let infer_def env d : Env.t =
   match d.it with
diff --git a/spectec/src/il2al/animate.ml b/spectec/src/il2al/animate.ml
index 5308fefc99..a37c25b92d 100644
--- a/spectec/src/il2al/animate.ml
+++ b/spectec/src/il2al/animate.ml
@@ -48,6 +48,19 @@ let is_assign env (tag, prem, _) =
   | Assign frees -> subset (diff (free_prem false prem) {empty with varid = (Set.of_list frees)}) env
   | _ -> false
 
+(* conversion between quantifiers and id lists *)
+let ids_of_quants qs =
+  List.filter_map (fun q ->
+    match q.it with
+    | ExpP (id, _) -> Some id.it
+    | _ -> None
+  ) qs
+
+let quants_of_ids ids =
+  List.map (fun id ->
+    ExpP (id $ no_region, VarT ("?" $ no_region, []) $ no_region) $ no_region
+  ) ids
+
 (* Rewrite iterexp of IterPr *)
 let rewrite (iter, xes) e =
   let rewrite' e' =
@@ -67,6 +80,10 @@ let rewrite_id (_, xes) id =
     | _ -> None
   ) xes
   |> get_or_else id
+let rewrite_quant iterexp q =
+  match q.it with
+  | ExpP (id, t) -> ExpP (rewrite_id iterexp id.it $ id.at, t) $ q.at
+  | _ -> q
 let rec rewrite_iterexp' iterexp pr =
   let transformer =
     { Il_walk.base_transformer with transform_exp = rewrite iterexp } in
@@ -74,9 +91,9 @@ let rec rewrite_iterexp' iterexp pr =
   match pr with
   | RulePr (id, args, mixop, e) -> RulePr (id, args, mixop, new_ e)
   | IfPr e -> IfPr (new_ e)
-  | LetPr (e1, e2, ids) ->
-    let new_ids = List.map (rewrite_id iterexp) ids in
-    LetPr (new_ e1, new_ e2, new_ids)
+  | LetPr (qs, e1, e2) ->
+    let new_qs = List.map (rewrite_quant iterexp) qs in
+    LetPr (new_qs, new_ e1, new_ e2)
   | ElsePr -> ElsePr
   | IterPr (pr, (iter, xes)) -> IterPr (rewrite_iterexp iterexp pr, (iter, xes |> List.map (fun (x, e) -> (x, new_ e))))
 and rewrite_iterexp iterexp pr = Source.map (rewrite_iterexp' iterexp) pr
@@ -97,6 +114,10 @@ let recover_id (_, xes) id =
     | _ -> None
   ) xes
   |> get_or_else id
+let recover_quant iterexp q =
+  match q.it with
+  | ExpP (id, t) -> ExpP (recover_id iterexp id.it $ id.at, t) $ q.at
+  | _ -> q
 let rec recover_iterexp' iterexp pr =
   let transformer =
     { Il_walk.base_transformer with transform_exp = recover iterexp } in
@@ -104,9 +125,9 @@ let rec recover_iterexp' iterexp pr =
   match pr with
   | RulePr (id, args, mixop, e) -> RulePr (id, args, mixop, new_ e)
   | IfPr e -> IfPr (new_ e)
-  | LetPr (e1, e2, ids) ->
-    let new_ids = List.map (recover_id iterexp) ids in
-    LetPr (new_ e1, new_ e2, new_ids)
+  | LetPr (qs, e1, e2) ->
+    let new_qs = List.map (recover_quant iterexp) qs in
+    LetPr (new_qs, new_ e1, new_ e2)
   | ElsePr -> ElsePr
   | IterPr (pr, (iter, xes)) -> IterPr (recover_iterexp iterexp pr, (iter, xes |> List.map (fun (x, e) -> (x, new_ e))))
 and recover_iterexp iterexp pr = Source.map (recover_iterexp' iterexp) pr
@@ -114,14 +135,14 @@ and recover_iterexp iterexp pr = Source.map (recover_iterexp' iterexp) pr
 (* is this assign premise a if-let? *)
 let is_cond_assign prem =
   match prem.it with
-  | LetPr ({it = CaseE (_, _); _}, _, _) -> true
+  | LetPr (_, {it = CaseE (_, _); _}, _) -> true
   | _ -> false
 
 (* is this assign premise encoded premise for popping one value? *)
 let is_pop env row =
   is_assign env row &&
   match (unwrap row).it with
-  | LetPr (_, {it = CallE (_, {it = ExpA n; _} :: _); note; _}, _) when Il.Print.string_of_typ note = "stackT" ->
+  | LetPr (_, _, {it = CallE (_, {it = ExpA n; _} :: _); note; _}) when Il.Print.string_of_typ note = "stackT" ->
     (match n.it with
     | NumE (`Nat i) -> Z.equal i (Z.one)
     | _ -> false)
@@ -272,7 +293,7 @@ let rows_of_eq vars len i l r at =
   |> List.filter_map (fun frees ->
     let covering_vars = List.filter_map (index_of len vars) frees in
     if List.length frees = List.length covering_vars then (
-      Some (Assign frees, LetPr (l, r, frees) $ at, [i] @ covering_vars) )
+      Some (Assign frees, LetPr (quants_of_ids frees, l, r) $ at, [i] @ covering_vars) )
     else
       None
   )
@@ -290,7 +311,8 @@ let rec rows_of_prem vars len i p =
         @ rows_of_eq vars len i l { r with it = TheE r } p.at
       | _ -> [ Condition, p, [i] ]
     )
-  | LetPr (_, _, targets) ->
+  | LetPr (qs, _, _) ->
+    let targets = ids_of_quants qs in
     let covering_vars = List.filter_map (index_of len vars) targets in
     [ Assign targets, p, [i] @ covering_vars ]
   | RulePr (_, _, _, { it = TupE args; _ }) ->
diff --git a/spectec/src/il2al/encode.ml b/spectec/src/il2al/encode.ml
index 149f1ae9b6..63c9d9da2e 100644
--- a/spectec/src/il2al/encode.ml
+++ b/spectec/src/il2al/encode.ml
@@ -61,6 +61,7 @@ let free_ids e =
   (free_exp false e)
   .varid
   |> Set.elements
+  |> List.map (fun id -> ExpP (id $ no_region, mk_varT "?") $ no_region)
 
 let dim e =
   let t = (NumT `NatT $ no_region) in
@@ -91,7 +92,7 @@ let encode_inner_stack context_opt stack =
       []
     else
       let unused = TupE dropped $$ no_region % (mk_varT "unusedT") in
-      [LetPr (unused, mk_varE "unused" "unusedT", free_ids unused) $ no_region]
+      [LetPr (free_ids unused, unused, mk_varE "unused" "unusedT") $ no_region]
   in
 
   match es with
@@ -101,13 +102,13 @@ let encode_inner_stack context_opt stack =
       match context_opt with
       | None -> assert false
       | Some e ->
-        Some (LetPr (e, mk_varE "input" "inputT", free_ids e) $ e.at), unused_prems
+        Some (LetPr (free_ids e, e, mk_varE "input" "inputT") $ e.at), unused_prems
     )
   | _ ->
     (* ASSUMPTION: The top of the stack should be now the target instruction *)
     let winstr, operands = Lib.List.split_hd es in
 
-    let prem = LetPr (winstr, mk_varE "input" "inputT", free_ids winstr) $ winstr.at in
+    let prem = LetPr (free_ids winstr, winstr, mk_varE "input" "inputT") $ winstr.at in
     let prems = List.mapi (fun i e ->
       let s0 = ("stack" ^ string_of_int i) in
       let s1 = ("stack" ^ string_of_int (i+1)) in
@@ -138,7 +139,7 @@ let encode_stack stack =
     let e1 = { e with it = CaseE (mixop', TupE args' $$ no_region % (mk_varT "")) } in
     let e2 = (mk_varE "ctxt" "contextT") in
 
-    let pr = LetPr (e1, e2, free_ids e1) $ e2.at in
+    let pr = LetPr (free_ids e1, e1, e2) $ e2.at in
 
     let pr_opt, prs = encode_inner_stack (Some e) inner_stack in
     (
@@ -153,7 +154,7 @@ let encode_stack stack =
 let encode_lhs lhs =
   match lhs.it with
   | CaseE (Xl.Mixop.(Infix (Arg (), {it = Semicolon; _}, Arg ())), {it = TupE [z; stack]; _}) ->
-    let prem = LetPr (z, mk_varE "state" "stateT", free_ids z) $ z.at in
+    let prem = LetPr (free_ids z, z, mk_varE "state" "stateT") $ z.at in
     prem :: encode_stack stack
   | _ ->
     let stack = lhs in
diff --git a/spectec/src/il2al/free.ml b/spectec/src/il2al/free.ml
index af0f4029f7..047306712f 100644
--- a/spectec/src/il2al/free.ml
+++ b/spectec/src/il2al/free.ml
@@ -83,7 +83,7 @@ let rec free_prem ignore_listN prem =
   match prem.it with
   | RulePr (_id, args, _op, e) -> free_list fa args ++ f e
   | IfPr e -> f e
-  | LetPr (e1, e2, _ids) -> f e1 ++ f e2
+  | LetPr (_qs, e1, e2) -> f e1 ++ f e2
   | ElsePr -> empty
   | IterPr (prem', iter) ->
     let free1 = fp prem' in
diff --git a/spectec/src/il2al/il2al_util.ml b/spectec/src/il2al/il2al_util.ml
index 72e1826c4b..18e5893857 100644
--- a/spectec/src/il2al/il2al_util.ml
+++ b/spectec/src/il2al/il2al_util.ml
@@ -34,20 +34,26 @@ let prems_of_rule rule =
 
 let lhs_of_prem pr =
   match pr.it with
-  | LetPr (lhs, _, _) -> lhs
+  | LetPr (_, lhs, _) -> lhs
   | _ -> error pr.at "expected a LetPr"
 let rhs_of_prem pr =
   match pr.it with
-  | LetPr (_, rhs, _) -> rhs
+  | LetPr (_, _, rhs) -> rhs
   | _ -> error pr.at "expected a LetPr"
 let replace_lhs lhs pr =
   let open Il.Free in
   match pr.it with
-  | LetPr (lhs', rhs, _) ->
+  | LetPr (qs, lhs', rhs) ->
     if Il.Eq.eq_exp lhs lhs' then
       pr
     else
-      { pr with it = LetPr (lhs, rhs, (free_exp lhs).varid |> Set.elements) }
+      let free = free_exp lhs in
+      let qs' = List.filter (fun q ->
+        match q.it with
+        | ExpP (id, _) -> Set.mem id.it free.varid
+        | _ -> true
+      ) qs in
+      { pr with it = LetPr (qs', lhs, rhs) }
   | _ -> error pr.at "expected a LetPr"
 
 let case_of_case e =
@@ -87,7 +93,7 @@ let split_last_case mixop = Option.get (split_last_case' mixop)
 
 let is_let_prem_with_rhs_type t prem =
   match prem.it with
-  | LetPr (_, e, _) ->
+  | LetPr (_, _, e) ->
     (match e.note.it with
     | VarT (id, []) -> id.it = t
     | _ -> false
diff --git a/spectec/src/il2al/il_walk.ml b/spectec/src/il2al/il_walk.ml
index 90d5c842ef..0b42810697 100644
--- a/spectec/src/il2al/il_walk.ml
+++ b/spectec/src/il2al/il_walk.ml
@@ -72,7 +72,7 @@ and transform_prem t p =
   let it = match p.it with
     | RulePr (id, as1, op, e) -> RulePr (id, List.map (transform_arg t) as1, op, transform_exp t e)
     | IfPr e -> IfPr (transform_exp t e)
-    | LetPr (e1, e2, ss) -> LetPr (transform_exp t e1, transform_exp t e2, ss)
+    | LetPr (qs, e1, e2) -> LetPr (qs, transform_exp t e1, transform_exp t e2)
     | ElsePr -> ElsePr
     | IterPr (p, ie) -> IterPr (transform_prem t p, transform_iterexp t ie)
   in
diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml
index 4d56bea331..a1b1966df1 100644
--- a/spectec/src/il2al/translate.ml
+++ b/spectec/src/il2al/translate.ml
@@ -142,7 +142,7 @@ let is_winstr_prem = is_let_prem_with_rhs_type "inputT"
 
 let lhs_of_prem pr =
   match pr.it with
-  | Il.LetPr (lhs, _, _) -> lhs
+  | Il.LetPr (_, lhs, _) -> lhs
   | _ -> Error.error pr.at "prose translation" "expected a LetPr"
 
 let rec is_wasm_value e =
@@ -979,7 +979,8 @@ and translate_prem prem =
   match prem.it with
   | Il.IfPr exp -> [ ifI (translate_exp exp, [], []) ~at ]
   | Il.ElsePr -> [ otherwiseI [] ~at ]
-  | Il.LetPr (exp1, exp2, ids) ->
+  | Il.LetPr (qs, exp1, exp2) ->
+    let ids = List.filter_map (fun q -> match q.it with (Il.ExpP (id, _)) -> Some id.it | _ -> None) qs in
     init_lhs_id ();
     translate_letpr exp1 exp2 ids
   | Il.RulePr (id, args, _, exp) ->
diff --git a/spectec/src/il2al/unify.ml b/spectec/src/il2al/unify.ml
index 4db51215a3..170aa34b94 100644
--- a/spectec/src/il2al/unify.ml
+++ b/spectec/src/il2al/unify.ml
@@ -40,6 +40,13 @@ let imap : idxs ref = ref Map.empty
 let init_env frees = { idxs = !imap; frees }
 
 
+let ids_of_quants qs =
+  List.filter_map (fun q ->
+    match q.it with
+    | ExpP (id, _) -> Some id.it
+    | _ -> None
+  ) qs
+
 let gen_new_unified ?prefix env ty =
   let var =
     match prefix with
@@ -58,6 +65,11 @@ let rename_string _env s =
 
 let rename_id env id = { id with it = rename_string env id.it }
 
+let rename_quant env q =
+  match q.it with
+  | ExpP (id, t) -> ExpP (rename_id env id, t) $ q.at
+  | _ -> q
+
 let rename_iterexp env (iter, ides) = (iter, List.map (fun (id, e) -> (rename_id env id, e)) ides)
 
 let rename_exp env exp =
@@ -68,7 +80,7 @@ let rename_exp env exp =
 
 let rename_prem env p =
   {p with it = match p.it with
-  | LetPr (e1, e2, ss) -> LetPr (e1, e2, List.map (rename_string env) ss)
+  | LetPr (qs, e1, e2) -> LetPr (List.map (rename_quant env) qs, e1, e2)
   | p' -> p' }
 
 let rename_rule_def (env, rd) =
@@ -319,14 +331,14 @@ let unify_enc env premss encs =
 
 let is_encoded_ctxt pr =
   match pr.it with
-  | LetPr (_, e, _) ->
+  | LetPr (_, _, e) ->
     (match e.note.it with
     | VarT (id, []) -> List.mem id.it ["inputT"; "stackT"; "contextT"]
     | _ -> false)
   | _ -> false
 let is_encoded_pop_or_winstr pr =
   match pr.it with
-  | LetPr (_, e, _) ->
+  | LetPr (_, _, e) ->
     (match e.note.it with
     | VarT (id, []) -> List.mem id.it ["inputT"; "stackT"]
     | _ -> false)
@@ -433,7 +445,7 @@ let unify_rule_def (env: env) (rule: rule_def) : rule_def =
             List.concat_map
               (fun p ->
                 match p.it with
-                | LetPr (_, _, ids) -> ids
+                | LetPr (qs, _, _) -> ids_of_quants qs
                 | _ -> assert false
               )
               pops
@@ -461,7 +473,7 @@ let reorder_unified_args args prems =
   (* Helpers *)
   let has_uarg_on_rhs p =
     match p.it with
-    | LetPr (_, {it = VarE id; _}, _) -> is_unified_id id.it
+    | LetPr (_, _, {it = VarE id; _}) -> is_unified_id id.it
     | _ -> false
   in
   let on_rhs p a =
diff --git a/spectec/src/middlend/sideconditions.ml b/spectec/src/middlend/sideconditions.ml
index 5000d56768..6872b78e11 100644
--- a/spectec/src/middlend/sideconditions.ml
+++ b/spectec/src/middlend/sideconditions.ml
@@ -131,7 +131,7 @@ let rec t_prem env prem =
   (match prem.it with
   | RulePr (_, args, _, exp) -> List.concat_map (t_arg env) args @ t_exp env exp
   | IfPr e -> t_exp env e
-  | LetPr (e1, e2, _) -> t_exp env e1 @ t_exp env e2
+  | LetPr (_qs, e1, e2) -> t_exp env e1 @ t_exp env e2
   | ElsePr -> []
   | IterPr (prem, iterexp)
   -> iter_side_conditions env iterexp @
diff --git a/spectec/src/middlend/sub.ml b/spectec/src/middlend/sub.ml
index 1aa0fe5d91..38dcc24ca2 100644
--- a/spectec/src/middlend/sub.ml
+++ b/spectec/src/middlend/sub.ml
@@ -216,7 +216,7 @@ and t_params env = List.map (t_param env)
 and t_prem' env = function
   | RulePr (id, args, mixop, exp) -> RulePr (id, t_args env args, mixop, t_exp env exp)
   | IfPr e -> IfPr (t_exp env e)
-  | LetPr (e1, e2, ids) -> LetPr (t_exp env e1, t_exp env e2, ids)
+  | LetPr (qs, e1, e2) -> LetPr (t_params env qs, t_exp env e1, t_exp env e2)
   | ElsePr -> ElsePr
   | IterPr (prem, iterexp) -> IterPr (t_prem env prem, t_iterexp env iterexp)
 
diff --git a/spectec/src/middlend/totalize.ml b/spectec/src/middlend/totalize.ml
index ade0ec336c..feb8e5ee98 100644
--- a/spectec/src/middlend/totalize.ml
+++ b/spectec/src/middlend/totalize.ml
@@ -154,7 +154,7 @@ and t_params env = List.map (t_param env)
 and t_prem' env = function
   | RulePr (id, args, mixop, exp) -> RulePr (id, t_args env args, mixop, t_exp env exp)
   | IfPr e -> IfPr (t_exp env e)
-  | LetPr (e1, e2, ids) -> LetPr (t_exp env e1, t_exp env e2, ids)
+  | LetPr (qs, e1, e2) -> LetPr (t_params env qs, t_exp env e1, t_exp env e2)
   | ElsePr -> ElsePr
   | IterPr (prem, iterexp) -> IterPr (t_prem env prem, t_iterexp env iterexp)
 
diff --git a/spectec/src/middlend/unthe.ml b/spectec/src/middlend/unthe.ml
index fb2155f825..015d1bc15c 100644
--- a/spectec/src/middlend/unthe.ml
+++ b/spectec/src/middlend/unthe.ml
@@ -198,7 +198,7 @@ and t_prem' n prem : eqns * prem' =
   match prem with
   | RulePr (a, args, b, exp) -> binary (fun n x -> t_list t_arg n x Fun.id) t_exp n (args, exp) (fun (args', exp') -> RulePr (a, args', b, exp'))
   | IfPr e -> unary t_exp n e (fun e' -> IfPr e')
-  | LetPr (e1, e2, ids) -> binary t_exp t_exp n (e1, e2) (fun (e1', e2') -> LetPr (e1', e2', ids))
+  | LetPr (qs, e1, e2) -> binary t_exp t_exp n (e1, e2) (fun (e1', e2') -> LetPr (qs, e1', e2'))
   | ElsePr -> [], prem
   | IterPr (prem, iterexp) ->
     let eqns1, prem' = t_prem n prem in