diff --git a/docs/about/formalities.md b/docs/about/formalities.md
index b2b01f1..57871b4 100644
--- a/docs/about/formalities.md
+++ b/docs/about/formalities.md
@@ -116,7 +116,7 @@ n fresh
 
 // 1 + n! premises
 // trace pairs: i ∈ [1..(n! + 1)], premise[i] -- conclusion
-c, γ*  ⊢ a_1, ..., a_n
+c, γ*  ⊢ a_1, ..., a_n, δ*
 ∀ I ⊆ {1, ..., n}.
 	c, γ* ⊢ { a_i | i ∈ I }, δ*
 	OR