diff --git a/docs/about/progress.md b/docs/about/progress.md
index 70380d6..40c97dc 100644
--- a/docs/about/progress.md
+++ b/docs/about/progress.md
@@ -69,17 +69,19 @@ Thoughts
 	- the meaning of `true` and existence of methods.
 		- undefined behaviour and `true`?
 	- how does this relate to the denotation stuff from before?
-* formal rules and the sequent calculus
+
+# formal rules and the sequent calculus
+Check formalities.md.
 	- simple rules
 	- type constructor rules
 	- recursion and cyclic proofs
 * next steps?
-	- implementation: sequent calculus based subtyping decider
-		- simple rules, should be fairly simple
-		- type constructors, straightforward hopefully
-		- recursion and cyclic proofs... `¯\_(ツ)_/¯`
 	- formals:
 		- formulate theorems
 			- if we use semantic subtyping, isn't it enough to
 			  prove subtyping sound with regards to set denotation?
 		- specify term language?
+	- implementation: sequent calculus based subtyping decider
+		- simple rules, should be fairly simple
+		- type constructors, straightforward hopefully
+		- recursion and cyclic proofs... `¯\_(ツ)_/¯`