diff --git a/report/chapters/03_theory.typ b/report/chapters/03_theory.typ
index 31a3143..4271836 100644
--- a/report/chapters/03_theory.typ
+++ b/report/chapters/03_theory.typ
@@ -173,6 +173,8 @@ Finally, expressions can be used in statements, which are special constructs tha
 
 #smallcaps[T-Annot] is a rule which handles Python type annotations. It states that the type checker must take note of type hints in the context.
 
+#smallcaps[T-Assign] handles assignments to variables. For an assignment to be valid, the value must be of the same type as the variable's type (modulo subsumption, #smallcaps[T-Sub]).
+
 #smallcaps[T-Seq] allows sequences of statements.
 
 #smallcaps[T-IfElse], like #smallcaps[T-Tern] is a stricter version of how Python processes `if` statements. Indeed, Midas will not allow leaking context from inside the bodies of any branch. If a variable is declared inside an `if` statement, Midas will not allow references outside of it.
diff --git a/report/chapters/03_theory/typing.typ b/report/chapters/03_theory/typing.typ
index 79d38f3..a470788 100644
--- a/report/chapters/03_theory/typing.typ
+++ b/report/chapters/03_theory/typing.typ
@@ -95,6 +95,13 @@
     $Gamma tack "x": "T" tack.l Gamma, "x": "T"$,
     ```py x: T```,
   ),
+  rule(
+    "T-Assign",
+    $Gamma tack "x": "T"$,
+    $Gamma tack "t": "T"$,
+    $Gamma tack "x" = "t" tack.l Gamma$,
+    ```py x = t```,
+  ),
   rule(
     "T-Seq",
     $Gamma tack "s"_1 tack.l Gamma'$,
diff --git a/report/chapters/04_implementation/05_python_checking.typ b/report/chapters/04_implementation/05_python_checking.typ
index 1c0f500..190ad66 100644
--- a/report/chapters/04_implementation/05_python_checking.typ
+++ b/report/chapters/04_implementation/05_python_checking.typ
@@ -121,7 +121,7 @@ During parsing, a statement such as ```python foo: int = 3```, represented in Py
 
 This method basically materializes #smallcaps[T-Annot] from @tab:typing-statements.
 
-Handling the variable assignment part is a bit more involved, because Python (and our type checker) allows both assigning to multiple targets simultaneously (@fig:python-visit_assign_stmt:3) and assigning to attributes and subscripts (not only variables). This is the reason we use a `match` statement in @fig:python-visit_assign_stmt.
+Handling the variable assignment part is a bit more involved, because Python (and our type checker) allows both assigning to multiple targets simultaneously (@fig:python-visit_assign_stmt:3) and assigning to attributes and subscripts (not only variables). This is the reason we use a `match` statement in @fig:python-visit_assign_stmt. This function embodies #smallcaps[T-Assign].
 
 #codly(
   ranges: (