diff --git a/docs/docs/reference/principled-meta-programming.md b/docs/docs/reference/principled-meta-programming.md
index 7041f787be32..774452b956ec 100644
--- a/docs/docs/reference/principled-meta-programming.md
+++ b/docs/docs/reference/principled-meta-programming.md
@@ -751,7 +751,7 @@ environments and terms.
                            Es |- 't: expr T
 
 The meta theory of a slightly simplified variant 2-stage variant of this calculus
-is studied [separatey](../simple-smp.md)
+is studied [separately](simple-smp.md).
 
 ## Going Further
 
diff --git a/docs/docs/reference/simple-smp.md b/docs/docs/reference/simple-smp.md
index bc7b4b68c617..752da90c24b8 100644
--- a/docs/docs/reference/simple-smp.md
+++ b/docs/docs/reference/simple-smp.md
@@ -3,10 +3,6 @@ layout: doc-page
 title: "The Meta-theory of Symmetric Meta-programming"
 ---
 
-# The Meta-theory of Symmetric Meta-programming
-
-23.12.2017
-
 This note presents a simplified variant of
 [principled meta-programming](./principled-meta-programming.md)
 and sketches its soundness proof. The variant treats only dialogues