Merge pull request #4517 from dotty-staging/unbreak-link-proofs

Docs: Unbreak link to proofs

Author: Blaisorblade

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
 

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