Bump Version & Fix Typos

.i18n/Game.pot

@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.6.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: Thu Feb 29 17:42:23 2024\n"
+"POT-Creation-Date: Tue May 14 13:24:37 2024\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: en\n"
@@ -3236,6 +3236,10 @@ msgid "\n"
 "\n"
 "Below, you're provided with a whirlwind tour of the notation at play as well as a bit of motivation for why the notation looks the way it does. This is all done through a single example. Many of the details will seem lacking; The concepts covered here will be addressed with more detail during the tutorial worlds of this game.\n"
 "\n"
+"# Redux\n"
+"\n"
+"Each tutorial world is accompanied by a **Redux World** with the same subtitle. These worlds are optional, don't have any flavor text, and challenge you to solve the exact same set of levels in a different way. These worlds probably do not belong in a puzzle game, but I found the exercise helpful in garnering a computer-sciencey intuition about the interplay between proof terms and tactics in Lean 4.\n"
+"\n"
 "# Building some notation\n"
 "Consider the following argument stated in natural language:\n"
 "\n"