diff --git a/spectec/doc/semantics/il/0-aux.spectec b/spectec/doc/semantics/il/0-aux.spectec
index 7f322499c6..16b3bff37c 100644
--- a/spectec/doc/semantics/il/0-aux.spectec
+++ b/spectec/doc/semantics/il/0-aux.spectec
@@ -13,3 +13,8 @@ def $equiv_(syntax X, x_1*, x_2*) = false  -- otherwise
 def $transpose_(syntax X, X**) : X**
 def $transpose_(syntax X, eps^n) = eps
 def $transpose_(syntax X, (x_1 x*)*) = x_1* $transpose_(X, x**)
+
+
+def $forall(bool*) : bool 
+def $forall(eps) = true
+def $forall(bool_1 bool*) = bool_1 /\ $forall(bool*)
diff --git a/spectec/doc/semantics/il/6-typing.spectec b/spectec/doc/semantics/il/6-typing.spectec
index da62e48d33..55bb1c08dd 100644
--- a/spectec/doc/semantics/il/6-typing.spectec
+++ b/spectec/doc/semantics/il/6-typing.spectec
@@ -45,16 +45,16 @@ rule Sub_typ/struct:
   E |- t_1 <: t_2
   -- Expand_typ: E |- t_1 => STRUCT tf_1*
   -- Expand_typ: E |- t_2 => STRUCT tf_2*
-  -- (if (a `: t_2a `- `{q*} pr*) = tf_2)*
-  -- (if (a `: t_1a `- `{q*} pr*) <- tf_1*)*
+  -- (if (a `: t_2a `- `{q*} pr_2*) = tf_2)*
+  -- (if (a `: t_1a `- `{q*} pr_1*) <- tf_1* /\ $forall((pr_2 <- pr_1*)*))*
   -- (Sub_typ: E |- t_1a <: t_2a)*
 
 rule Sub_typ/variant:
   E |- t_1 <: t_2
   -- Expand_typ: E |- t_1 => VARIANT tc_1*
   -- Expand_typ: E |- t_2 => VARIANT tc_2*
-  -- (if (m `: t_1a `- `{q*} pr*) = tc_1)*
-  -- (if (m `: t_2a `- `{q*} pr*) <- tc_2*)*
+  -- (if (m `: t_1a `- `{q*} pr_1*) = tc_1)*
+  -- (if (m `: t_2a `- `{q*} pr_2*) <- tc_2* /\ $forall((pr_2 <- pr_1*)*))*
   -- (Sub_typ: E |- t_1a <: t_2a)*
 
 rule Sub_typ/iter: