diff --git a/Dockerfile b/Dockerfile
index 918f584..988760b 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -25,4 +25,4 @@ RUN lake clean && lake build
 
 WORKDIR /game/lake-packages/GameServer/server/build/bin/
 
-CMD ./gameserver --server /game/ Game NNG
+CMD ./gameserver --server /game/
diff --git a/Game.lean b/Game.lean
index 2ac4722..87bf559 100644
--- a/Game.lean
+++ b/Game.lean
@@ -11,7 +11,6 @@ import Game.Levels.AdvAddition
 import Game.Levels.AdvMultiplication
 --import Game.Levels.Inequality
 
-Game "NNG"
 Title "Natural Number Game"
 Introduction
 "
diff --git a/Game/Levels/Addition.lean b/Game/Levels/Addition.lean
index af8de39..681e28b 100644
--- a/Game/Levels/Addition.lean
+++ b/Game/Levels/Addition.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Addition.Level_6
 
-Game "NNG"
+
 World "Addition"
 Title "Addition World"
 
diff --git a/Game/Levels/Addition/Level_1.lean b/Game/Levels/Addition/Level_1.lean
index 46acaab..aaac5d4 100644
--- a/Game/Levels/Addition/Level_1.lean
+++ b/Game/Levels/Addition/Level_1.lean
@@ -1,7 +1,6 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
 World "Addition"
 Level 1
 Title "the induction tactic."
diff --git a/Game/Levels/Addition/Level_2.lean b/Game/Levels/Addition/Level_2.lean
index f82b29b..f3b6e23 100644
--- a/Game/Levels/Addition/Level_2.lean
+++ b/Game/Levels/Addition/Level_2.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Addition.Level_1
 
-Game "NNG"
+
 World "Addition"
 Level 2
 Title "add_assoc (associativity of addition)"
diff --git a/Game/Levels/Addition/Level_3.lean b/Game/Levels/Addition/Level_3.lean
index 0cee2d0..3da68c9 100644
--- a/Game/Levels/Addition/Level_3.lean
+++ b/Game/Levels/Addition/Level_3.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Addition.Level_2
 
-Game "NNG"
+
 World "Addition"
 Level 3
 Title "succ_add"
diff --git a/Game/Levels/Addition/Level_4.lean b/Game/Levels/Addition/Level_4.lean
index c8d944a..3600c75 100644
--- a/Game/Levels/Addition/Level_4.lean
+++ b/Game/Levels/Addition/Level_4.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Addition.Level_3
 
-Game "NNG"
+
 World "Addition"
 Level 4
 Title "`add_comm` (boss level)"
diff --git a/Game/Levels/Addition/Level_5.lean b/Game/Levels/Addition/Level_5.lean
index 03fe7ba..962658a 100644
--- a/Game/Levels/Addition/Level_5.lean
+++ b/Game/Levels/Addition/Level_5.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Addition.Level_4
 
-Game "NNG"
+
 World "Addition"
 Level 5
 Title "succ_eq_add_one"
diff --git a/Game/Levels/Addition/Level_6.lean b/Game/Levels/Addition/Level_6.lean
index 32837f9..95c1990 100644
--- a/Game/Levels/Addition/Level_6.lean
+++ b/Game/Levels/Addition/Level_6.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Addition.Level_5
 
-Game "NNG"
+
 World "Addition"
 Level 6
 Title "add_right_comm"
diff --git a/Game/Levels/AdvAddition.lean b/Game/Levels/AdvAddition.lean
index 5aa41ff..ad49125 100644
--- a/Game/Levels/AdvAddition.lean
+++ b/Game/Levels/AdvAddition.lean
@@ -1,6 +1,6 @@
 import Game.Levels.AdvAddition.Level_13
 
-Game "NNG"
+
 World "AdvAddition"
 Title "Advanced Addition World"
 
diff --git a/Game/Levels/AdvAddition/Level_1.lean b/Game/Levels/AdvAddition/Level_1.lean
index 1a6c9d3..b2f1475 100644
--- a/Game/Levels/AdvAddition/Level_1.lean
+++ b/Game/Levels/AdvAddition/Level_1.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.AdvAddition
 import Game.Levels.Addition
 
-Game "NNG"
+
 World "AdvAddition"
 Level 1
 Title "`succ_inj`. A function."
diff --git a/Game/Levels/AdvAddition/Level_10.lean b/Game/Levels/AdvAddition/Level_10.lean
index 8576a5c..679f0c0 100644
--- a/Game/Levels/AdvAddition/Level_10.lean
+++ b/Game/Levels/AdvAddition/Level_10.lean
@@ -1,7 +1,7 @@
 import Game.Levels.AdvAddition.Level_9
 import Std.Tactic.RCases
 
-Game "NNG"
+
 World "AdvAddition"
 Level 10
 Title "add_left_eq_zero"
diff --git a/Game/Levels/AdvAddition/Level_11.lean b/Game/Levels/AdvAddition/Level_11.lean
index 3765003..85d0564 100644
--- a/Game/Levels/AdvAddition/Level_11.lean
+++ b/Game/Levels/AdvAddition/Level_11.lean
@@ -1,6 +1,6 @@
 import Game.Levels.AdvAddition.Level_10
 
-Game "NNG"
+
 World "AdvAddition"
 Level 11
 Title "add_right_eq_zero"
diff --git a/Game/Levels/AdvAddition/Level_12.lean b/Game/Levels/AdvAddition/Level_12.lean
index 4b5975c..0223976 100644
--- a/Game/Levels/AdvAddition/Level_12.lean
+++ b/Game/Levels/AdvAddition/Level_12.lean
@@ -1,7 +1,7 @@
 import Game.Levels.AdvAddition.Level_11
 
 
-Game "NNG"
+
 World "AdvAddition"
 Level 12
 Title "add_one_eq_succ"
diff --git a/Game/Levels/AdvAddition/Level_13.lean b/Game/Levels/AdvAddition/Level_13.lean
index 7c828b3..0da02c2 100644
--- a/Game/Levels/AdvAddition/Level_13.lean
+++ b/Game/Levels/AdvAddition/Level_13.lean
@@ -1,6 +1,6 @@
 import Game.Levels.AdvAddition.Level_12
 
-Game "NNG"
+
 World "AdvAddition"
 Level 13
 Title "ne_succ_self"
diff --git a/Game/Levels/AdvAddition/Level_2.lean b/Game/Levels/AdvAddition/Level_2.lean
index e9ded37..045f6f8 100644
--- a/Game/Levels/AdvAddition/Level_2.lean
+++ b/Game/Levels/AdvAddition/Level_2.lean
@@ -1,7 +1,7 @@
 import Game.Levels.AdvAddition.Level_1
 
 
-Game "NNG"
+
 World "AdvAddition"
 Level 2
 Title "succ_succ_inj"
diff --git a/Game/Levels/AdvAddition/Level_3.lean b/Game/Levels/AdvAddition/Level_3.lean
index 1b73c1c..842d528 100644
--- a/Game/Levels/AdvAddition/Level_3.lean
+++ b/Game/Levels/AdvAddition/Level_3.lean
@@ -1,7 +1,7 @@
 import Game.Levels.AdvAddition.Level_2
 
 
-Game "NNG"
+
 World "AdvAddition"
 Level 3
 Title "succ_eq_succ_of_eq"
diff --git a/Game/Levels/AdvAddition/Level_4.lean b/Game/Levels/AdvAddition/Level_4.lean
index bc086bd..99de300 100644
--- a/Game/Levels/AdvAddition/Level_4.lean
+++ b/Game/Levels/AdvAddition/Level_4.lean
@@ -1,6 +1,6 @@
 import Game.Levels.AdvAddition.Level_3
 
-Game "NNG"
+
 World "AdvAddition"
 Level 4
 Title "eq_iff_succ_eq_succ"
diff --git a/Game/Levels/AdvAddition/Level_5.lean b/Game/Levels/AdvAddition/Level_5.lean
index 2ea6561..415c7b6 100644
--- a/Game/Levels/AdvAddition/Level_5.lean
+++ b/Game/Levels/AdvAddition/Level_5.lean
@@ -1,7 +1,7 @@
 import Game.Levels.AdvAddition.Level_4
 
 
-Game "NNG"
+
 World "AdvAddition"
 Level 5
 Title "add_right_cancel"
diff --git a/Game/Levels/AdvAddition/Level_6.lean b/Game/Levels/AdvAddition/Level_6.lean
index 477246d..6a3eed1 100644
--- a/Game/Levels/AdvAddition/Level_6.lean
+++ b/Game/Levels/AdvAddition/Level_6.lean
@@ -1,6 +1,6 @@
 import Game.Levels.AdvAddition.Level_5
 
-Game "NNG"
+
 World "AdvAddition"
 Level 6
 Title "add_left_cancel"
diff --git a/Game/Levels/AdvAddition/Level_7.lean b/Game/Levels/AdvAddition/Level_7.lean
index a410db4..5f5a57a 100644
--- a/Game/Levels/AdvAddition/Level_7.lean
+++ b/Game/Levels/AdvAddition/Level_7.lean
@@ -1,6 +1,6 @@
 import Game.Levels.AdvAddition.Level_6
 
-Game "NNG"
+
 World "AdvAddition"
 Level 7
 Title "add_right_cancel_iff"
diff --git a/Game/Levels/AdvAddition/Level_8.lean b/Game/Levels/AdvAddition/Level_8.lean
index 9a4e109..707747f 100644
--- a/Game/Levels/AdvAddition/Level_8.lean
+++ b/Game/Levels/AdvAddition/Level_8.lean
@@ -1,7 +1,7 @@
 import Game.Levels.AdvAddition.Level_7
 
 
-Game "NNG"
+
 World "AdvAddition"
 Level 8
 Title "eq_zero_of_add_right_eq_self"
diff --git a/Game/Levels/AdvAddition/Level_9.lean b/Game/Levels/AdvAddition/Level_9.lean
index 842475f..9cf0be7 100644
--- a/Game/Levels/AdvAddition/Level_9.lean
+++ b/Game/Levels/AdvAddition/Level_9.lean
@@ -1,6 +1,6 @@
 import Game.Levels.AdvAddition.Level_8
 
-Game "NNG"
+
 World "AdvAddition"
 Level 9
 Title "succ_ne_zero"
diff --git a/Game/Levels/AdvMultiplication.lean b/Game/Levels/AdvMultiplication.lean
index da17b53..19bc752 100644
--- a/Game/Levels/AdvMultiplication.lean
+++ b/Game/Levels/AdvMultiplication.lean
@@ -4,7 +4,7 @@ import Game.Levels.AdvMultiplication.Level_3
 import Game.Levels.AdvMultiplication.Level_4
 
 
-Game "NNG"
+
 World "AdvMultiplication"
 Title "Advanced Multiplication World"
 
diff --git a/Game/Levels/AdvMultiplication/Level_1.lean b/Game/Levels/AdvMultiplication/Level_1.lean
index 28cdc7a..51b3534 100644
--- a/Game/Levels/AdvMultiplication/Level_1.lean
+++ b/Game/Levels/AdvMultiplication/Level_1.lean
@@ -1,7 +1,7 @@
 import Game.Levels.Multiplication
 import Game.Levels.AdvAddition
 
-Game "NNG"
+
 World "AdvMultiplication"
 Level 1
 Title "mul_pos"
diff --git a/Game/Levels/AdvMultiplication/Level_2.lean b/Game/Levels/AdvMultiplication/Level_2.lean
index efcf459..ae033b6 100644
--- a/Game/Levels/AdvMultiplication/Level_2.lean
+++ b/Game/Levels/AdvMultiplication/Level_2.lean
@@ -1,6 +1,6 @@
 import Game.Levels.AdvMultiplication.Level_1
 
-Game "NNG"
+
 World "AdvMultiplication"
 Level 2
 Title "eq_zero_or_eq_zero_of_mul_eq_zero"
diff --git a/Game/Levels/AdvMultiplication/Level_3.lean b/Game/Levels/AdvMultiplication/Level_3.lean
index 3861242..859dc02 100644
--- a/Game/Levels/AdvMultiplication/Level_3.lean
+++ b/Game/Levels/AdvMultiplication/Level_3.lean
@@ -1,7 +1,7 @@
 import Game.Levels.AdvMultiplication.Level_2
 
 
-Game "NNG"
+
 World "AdvMultiplication"
 Level 3
 Title "mul_eq_zero_iff"
diff --git a/Game/Levels/AdvMultiplication/Level_4.lean b/Game/Levels/AdvMultiplication/Level_4.lean
index c2f417b..b717ed6 100644
--- a/Game/Levels/AdvMultiplication/Level_4.lean
+++ b/Game/Levels/AdvMultiplication/Level_4.lean
@@ -1,6 +1,6 @@
 import Game.Levels.AdvMultiplication.Level_3
 
-Game "NNG"
+
 World "AdvMultiplication"
 Level 4
 Title "mul_left_cancel"
diff --git a/Game/Levels/AdvProposition.lean b/Game/Levels/AdvProposition.lean
index c02aca6..9af0523 100644
--- a/Game/Levels/AdvProposition.lean
+++ b/Game/Levels/AdvProposition.lean
@@ -10,7 +10,7 @@ import Game.Levels.AdvProposition.Level_9
 import Game.Levels.AdvProposition.Level_10
 
 
-Game "NNG"
+
 World "AdvProposition"
 Title "Advanced Proposition World"
 
diff --git a/Game/Levels/AdvProposition/Level_1.lean b/Game/Levels/AdvProposition/Level_1.lean
index 607a1c6..45f90ff 100644
--- a/Game/Levels/AdvProposition/Level_1.lean
+++ b/Game/Levels/AdvProposition/Level_1.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "AdvProposition"
 Level 1
 Title "the `split` tactic"
diff --git a/Game/Levels/AdvProposition/Level_10.lean b/Game/Levels/AdvProposition/Level_10.lean
index 1c75fcd..a69da5f 100644
--- a/Game/Levels/AdvProposition/Level_10.lean
+++ b/Game/Levels/AdvProposition/Level_10.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "AdvProposition"
 Level 10
 Title "The law of the excluded middle."
diff --git a/Game/Levels/AdvProposition/Level_2.lean b/Game/Levels/AdvProposition/Level_2.lean
index bd3200d..b2fe458 100644
--- a/Game/Levels/AdvProposition/Level_2.lean
+++ b/Game/Levels/AdvProposition/Level_2.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "AdvProposition"
 Level 2
 Title "the `rcases` tactic"
diff --git a/Game/Levels/AdvProposition/Level_3.lean b/Game/Levels/AdvProposition/Level_3.lean
index 9b78bbe..efaea9e 100644
--- a/Game/Levels/AdvProposition/Level_3.lean
+++ b/Game/Levels/AdvProposition/Level_3.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "AdvProposition"
 Level 3
 Title "and_trans"
diff --git a/Game/Levels/AdvProposition/Level_4.lean b/Game/Levels/AdvProposition/Level_4.lean
index 626eb44..6b36786 100644
--- a/Game/Levels/AdvProposition/Level_4.lean
+++ b/Game/Levels/AdvProposition/Level_4.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "AdvProposition"
 Level 4
 Title ""
diff --git a/Game/Levels/AdvProposition/Level_5.lean b/Game/Levels/AdvProposition/Level_5.lean
index 8894f59..d62ffd1 100644
--- a/Game/Levels/AdvProposition/Level_5.lean
+++ b/Game/Levels/AdvProposition/Level_5.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "AdvProposition"
 Level 5
 Title "Easter eggs."
diff --git a/Game/Levels/AdvProposition/Level_6.lean b/Game/Levels/AdvProposition/Level_6.lean
index 6db74a2..39e813a 100644
--- a/Game/Levels/AdvProposition/Level_6.lean
+++ b/Game/Levels/AdvProposition/Level_6.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "AdvProposition"
 Level 6
 Title "Or, and the `left` and `right` tactics."
diff --git a/Game/Levels/AdvProposition/Level_7.lean b/Game/Levels/AdvProposition/Level_7.lean
index bc84175..195fc91 100644
--- a/Game/Levels/AdvProposition/Level_7.lean
+++ b/Game/Levels/AdvProposition/Level_7.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "AdvProposition"
 Level 7
 Title "`or_symm`"
diff --git a/Game/Levels/AdvProposition/Level_8.lean b/Game/Levels/AdvProposition/Level_8.lean
index 1788386..ed1c068 100644
--- a/Game/Levels/AdvProposition/Level_8.lean
+++ b/Game/Levels/AdvProposition/Level_8.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "AdvProposition"
 Level 8
 Title "`and_or_distrib_left`"
diff --git a/Game/Levels/AdvProposition/Level_9.lean b/Game/Levels/AdvProposition/Level_9.lean
index 6a344b4..0ecb79d 100644
--- a/Game/Levels/AdvProposition/Level_9.lean
+++ b/Game/Levels/AdvProposition/Level_9.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "AdvProposition"
 Level 9
 Title "`exfalso` and proof by contradiction. "
diff --git a/Game/Levels/Function.lean b/Game/Levels/Function.lean
index 5e0ecdd..a296471 100644
--- a/Game/Levels/Function.lean
+++ b/Game/Levels/Function.lean
@@ -9,7 +9,7 @@ import Game.Levels.Function.Level_8
 import Game.Levels.Function.Level_9
 
 
-Game "NNG"
+
 World "Function"
 Title "Function World"
 
diff --git a/Game/Levels/Function/Level_1.lean b/Game/Levels/Function/Level_1.lean
index 8dee7c2..c196e00 100644
--- a/Game/Levels/Function/Level_1.lean
+++ b/Game/Levels/Function/Level_1.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 
 -- TODO: Cannot import level from different world.
 
-Game "NNG"
+
 World "Function"
 Level 1
 Title "the `exact` tactic"
diff --git a/Game/Levels/Function/Level_2.lean b/Game/Levels/Function/Level_2.lean
index 90edc63..572b5bf 100644
--- a/Game/Levels/Function/Level_2.lean
+++ b/Game/Levels/Function/Level_2.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Multiplication
 
-Game "NNG"
+
 World "Function"
 Level 2
 Title "the intro tactic"
diff --git a/Game/Levels/Function/Level_3.lean b/Game/Levels/Function/Level_3.lean
index 537b243..086c64c 100644
--- a/Game/Levels/Function/Level_3.lean
+++ b/Game/Levels/Function/Level_3.lean
@@ -1,6 +1,6 @@
 import Game.Metadata
 
-Game "NNG"
+
 World "Function"
 Level 3
 Title "the have tactic"
diff --git a/Game/Levels/Function/Level_4.lean b/Game/Levels/Function/Level_4.lean
index 84ea1e3..9ce7a97 100644
--- a/Game/Levels/Function/Level_4.lean
+++ b/Game/Levels/Function/Level_4.lean
@@ -1,6 +1,6 @@
 import Game.Metadata
 
-Game "NNG"
+
 World "Function"
 Level 4
 Title "the `apply` tactic"
diff --git a/Game/Levels/Function/Level_5.lean b/Game/Levels/Function/Level_5.lean
index 997e382..1d0cde1 100644
--- a/Game/Levels/Function/Level_5.lean
+++ b/Game/Levels/Function/Level_5.lean
@@ -1,6 +1,6 @@
 import Game.Metadata
 
-Game "NNG"
+
 World "Function"
 Level 5
 Title "P → (Q → P)"
diff --git a/Game/Levels/Function/Level_6.lean b/Game/Levels/Function/Level_6.lean
index 10fb7bf..9545227 100644
--- a/Game/Levels/Function/Level_6.lean
+++ b/Game/Levels/Function/Level_6.lean
@@ -1,6 +1,6 @@
 import Game.Metadata
 
-Game "NNG"
+
 World "Function"
 Level 6
 Title "(P → (Q → R)) → ((P → Q) → (P → R))"
diff --git a/Game/Levels/Function/Level_7.lean b/Game/Levels/Function/Level_7.lean
index 8d67e51..8a85af4 100644
--- a/Game/Levels/Function/Level_7.lean
+++ b/Game/Levels/Function/Level_7.lean
@@ -1,6 +1,6 @@
 import Game.Metadata
 
-Game "NNG"
+
 World "Function"
 Level 7
 Title "(P → Q) → ((Q → F) → (P → F))"
diff --git a/Game/Levels/Function/Level_8.lean b/Game/Levels/Function/Level_8.lean
index dd6ff08..93b445a 100644
--- a/Game/Levels/Function/Level_8.lean
+++ b/Game/Levels/Function/Level_8.lean
@@ -1,6 +1,6 @@
 import Game.Metadata
 
-Game "NNG"
+
 World "Function"
 Level 8
 Title "(P → Q) → ((Q → empty) → (P → empty))"
diff --git a/Game/Levels/Function/Level_9.lean b/Game/Levels/Function/Level_9.lean
index 1c78d54..4dd8885 100644
--- a/Game/Levels/Function/Level_9.lean
+++ b/Game/Levels/Function/Level_9.lean
@@ -1,6 +1,6 @@
 import Game.Metadata
 
-Game "NNG"
+
 World "Function"
 Level 9
 Title ""
diff --git a/Game/Levels/Inequality.lean b/Game/Levels/Inequality.lean
index 2080fd9..b9d6405 100644
--- a/Game/Levels/Inequality.lean
+++ b/Game/Levels/Inequality.lean
@@ -16,7 +16,7 @@ import Game.Levels.Inequality.Level_1
 -- import Game.Levels.Inequality.Level_16
 -- import Game.Levels.Inequality.Level_17
 
-Game "NNG"
+
 World "Inequality"
 Title "Inequality World"
 
diff --git a/Game/Levels/Inequality/Level_1.lean b/Game/Levels/Inequality/Level_1.lean
index 4a2e6dc..a8cd434 100644
--- a/Game/Levels/Inequality/Level_1.lean
+++ b/Game/Levels/Inequality/Level_1.lean
@@ -3,7 +3,7 @@ import Game.MyNat.LE
 import Game.Tactic.Use
 --import Mathlib.Tactic.Ring
 
-Game "NNG"
+
 World "Inequality"
 Level 1
 Title "the `use` tactic"
diff --git a/Game/Levels/Inequality/Level_10.lean b/Game/Levels/Inequality/Level_10.lean
index 1bea626..0da8012 100644
--- a/Game/Levels/Inequality/Level_10.lean
+++ b/Game/Levels/Inequality/Level_10.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 10
 Title ""
diff --git a/Game/Levels/Inequality/Level_11.lean b/Game/Levels/Inequality/Level_11.lean
index 6cea50d..0076673 100644
--- a/Game/Levels/Inequality/Level_11.lean
+++ b/Game/Levels/Inequality/Level_11.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 11
 Title ""
diff --git a/Game/Levels/Inequality/Level_12.lean b/Game/Levels/Inequality/Level_12.lean
index 985c0f8..d5e9cf2 100644
--- a/Game/Levels/Inequality/Level_12.lean
+++ b/Game/Levels/Inequality/Level_12.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 12
 Title ""
diff --git a/Game/Levels/Inequality/Level_13.lean b/Game/Levels/Inequality/Level_13.lean
index a4c338b..fe84020 100644
--- a/Game/Levels/Inequality/Level_13.lean
+++ b/Game/Levels/Inequality/Level_13.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 13
 Title ""
diff --git a/Game/Levels/Inequality/Level_14.lean b/Game/Levels/Inequality/Level_14.lean
index 2a234c9..6fcf998 100644
--- a/Game/Levels/Inequality/Level_14.lean
+++ b/Game/Levels/Inequality/Level_14.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 14
 Title ""
diff --git a/Game/Levels/Inequality/Level_15.lean b/Game/Levels/Inequality/Level_15.lean
index bb91ffc..a71820a 100644
--- a/Game/Levels/Inequality/Level_15.lean
+++ b/Game/Levels/Inequality/Level_15.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 15
 Title ""
diff --git a/Game/Levels/Inequality/Level_16.lean b/Game/Levels/Inequality/Level_16.lean
index 2be3ba1..2cb2737 100644
--- a/Game/Levels/Inequality/Level_16.lean
+++ b/Game/Levels/Inequality/Level_16.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 16
 Title ""
diff --git a/Game/Levels/Inequality/Level_17.lean b/Game/Levels/Inequality/Level_17.lean
index 250b9a4..5a9ec38 100644
--- a/Game/Levels/Inequality/Level_17.lean
+++ b/Game/Levels/Inequality/Level_17.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 17
 Title ""
diff --git a/Game/Levels/Inequality/Level_2.lean b/Game/Levels/Inequality/Level_2.lean
index d9cc6ba..b6c8c40 100644
--- a/Game/Levels/Inequality/Level_2.lean
+++ b/Game/Levels/Inequality/Level_2.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Mathlib.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 2
 Title "le_rfl"
diff --git a/Game/Levels/Inequality/Level_3.lean b/Game/Levels/Inequality/Level_3.lean
index af09753..2916341 100644
--- a/Game/Levels/Inequality/Level_3.lean
+++ b/Game/Levels/Inequality/Level_3.lean
@@ -3,7 +3,7 @@ import Game.MyNat.LE
 import Game.Tactic.Use
 import Std.Tactic.RCases
 
-Game "NNG"
+
 World "Inequality"
 Level 3
 Title "le_succ_of_le"
diff --git a/Game/Levels/Inequality/Level_4.lean b/Game/Levels/Inequality/Level_4.lean
index f36f404..844f26e 100644
--- a/Game/Levels/Inequality/Level_4.lean
+++ b/Game/Levels/Inequality/Level_4.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 4
 Title ""
diff --git a/Game/Levels/Inequality/Level_5.lean b/Game/Levels/Inequality/Level_5.lean
index 0d5e018..415514c 100644
--- a/Game/Levels/Inequality/Level_5.lean
+++ b/Game/Levels/Inequality/Level_5.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 5
 Title ""
diff --git a/Game/Levels/Inequality/Level_6.lean b/Game/Levels/Inequality/Level_6.lean
index 47a8387..2d4ac73 100644
--- a/Game/Levels/Inequality/Level_6.lean
+++ b/Game/Levels/Inequality/Level_6.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 6
 Title ""
diff --git a/Game/Levels/Inequality/Level_7.lean b/Game/Levels/Inequality/Level_7.lean
index 7a1c28f..c3b6283 100644
--- a/Game/Levels/Inequality/Level_7.lean
+++ b/Game/Levels/Inequality/Level_7.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 7
 Title ""
diff --git a/Game/Levels/Inequality/Level_8.lean b/Game/Levels/Inequality/Level_8.lean
index dc23d8f..ec8f4c3 100644
--- a/Game/Levels/Inequality/Level_8.lean
+++ b/Game/Levels/Inequality/Level_8.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 8
 Title ""
diff --git a/Game/Levels/Inequality/Level_9.lean b/Game/Levels/Inequality/Level_9.lean
index 1121b6e..3b17bc4 100644
--- a/Game/Levels/Inequality/Level_9.lean
+++ b/Game/Levels/Inequality/Level_9.lean
@@ -2,7 +2,7 @@ import Game.Metadata
 import Game.MyNat.LE
 import Game.Tactic.Use
 
-Game "NNG"
+
 World "Inequality"
 Level 9
 Title ""
diff --git a/Game/Levels/Multiplication.lean b/Game/Levels/Multiplication.lean
index 59a265d..c4c4c62 100644
--- a/Game/Levels/Multiplication.lean
+++ b/Game/Levels/Multiplication.lean
@@ -9,7 +9,7 @@ import Game.Levels.Multiplication.Level_8
 import Game.Levels.Multiplication.Level_9
 
 
-Game "NNG"
+
 World "Multiplication"
 Title "Multiplication World"
 
diff --git a/Game/Levels/Multiplication/Level_1.lean b/Game/Levels/Multiplication/Level_1.lean
index 42d0cca..d5c3491 100644
--- a/Game/Levels/Multiplication/Level_1.lean
+++ b/Game/Levels/Multiplication/Level_1.lean
@@ -1,7 +1,7 @@
 import Game.MyNat.Multiplication
 import Game.Levels.Addition
 
-Game "NNG"
+
 World "Multiplication"
 Level 1
 Title "zero_mul"
diff --git a/Game/Levels/Multiplication/Level_2.lean b/Game/Levels/Multiplication/Level_2.lean
index 0aa0be9..471b579 100644
--- a/Game/Levels/Multiplication/Level_2.lean
+++ b/Game/Levels/Multiplication/Level_2.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Multiplication.Level_1
 
-Game "NNG"
+
 World "Multiplication"
 Level 2
 Title "mul_one"
diff --git a/Game/Levels/Multiplication/Level_3.lean b/Game/Levels/Multiplication/Level_3.lean
index f6a052e..a21af2a 100644
--- a/Game/Levels/Multiplication/Level_3.lean
+++ b/Game/Levels/Multiplication/Level_3.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Multiplication.Level_2
 
-Game "NNG"
+
 World "Multiplication"
 Level 3
 Title "one_mul"
diff --git a/Game/Levels/Multiplication/Level_4.lean b/Game/Levels/Multiplication/Level_4.lean
index ba19285..2b7538f 100644
--- a/Game/Levels/Multiplication/Level_4.lean
+++ b/Game/Levels/Multiplication/Level_4.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Multiplication.Level_3
 
-Game "NNG"
+
 World "Multiplication"
 Level 4
 Title "mul_add"
diff --git a/Game/Levels/Multiplication/Level_5.lean b/Game/Levels/Multiplication/Level_5.lean
index f66e7af..48c64d1 100644
--- a/Game/Levels/Multiplication/Level_5.lean
+++ b/Game/Levels/Multiplication/Level_5.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Multiplication.Level_4
 
-Game "NNG"
+
 World "Multiplication"
 Level 5
 Title "mul_assoc"
diff --git a/Game/Levels/Multiplication/Level_6.lean b/Game/Levels/Multiplication/Level_6.lean
index a0f603a..d6f07ce 100644
--- a/Game/Levels/Multiplication/Level_6.lean
+++ b/Game/Levels/Multiplication/Level_6.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Multiplication.Level_5
 
-Game "NNG"
+
 World "Multiplication"
 Level 6
 Title "succ_mul"
diff --git a/Game/Levels/Multiplication/Level_7.lean b/Game/Levels/Multiplication/Level_7.lean
index f952ae6..a7a7520 100644
--- a/Game/Levels/Multiplication/Level_7.lean
+++ b/Game/Levels/Multiplication/Level_7.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Multiplication.Level_6
 
-Game "NNG"
+
 World "Multiplication"
 Level 7
 Title "add_mul"
diff --git a/Game/Levels/Multiplication/Level_8.lean b/Game/Levels/Multiplication/Level_8.lean
index e431fbd..a5c6c46 100644
--- a/Game/Levels/Multiplication/Level_8.lean
+++ b/Game/Levels/Multiplication/Level_8.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Multiplication.Level_7
 
-Game "NNG"
+
 World "Multiplication"
 Level 8
 Title "mul_comm"
diff --git a/Game/Levels/Multiplication/Level_9.lean b/Game/Levels/Multiplication/Level_9.lean
index e73a084..4019f09 100644
--- a/Game/Levels/Multiplication/Level_9.lean
+++ b/Game/Levels/Multiplication/Level_9.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Multiplication.Level_8
 
-Game "NNG"
+
 World "Multiplication"
 Level 9
 Title "mul_left_comm"
diff --git a/Game/Levels/Power.lean b/Game/Levels/Power.lean
index 0718843..e1b602f 100644
--- a/Game/Levels/Power.lean
+++ b/Game/Levels/Power.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Power.Level_8
 
-Game "NNG"
+
 World "Power"
 Title "Power World"
 
diff --git a/Game/Levels/Power/Level_1.lean b/Game/Levels/Power/Level_1.lean
index 5e58131..5bd6396 100644
--- a/Game/Levels/Power/Level_1.lean
+++ b/Game/Levels/Power/Level_1.lean
@@ -1,7 +1,7 @@
 import Game.Levels.Multiplication
 import Game.MyNat.Power
 
-Game "NNG"
+
 World "Power"
 Level 1
 Title "zero_pow_zero"
diff --git a/Game/Levels/Power/Level_2.lean b/Game/Levels/Power/Level_2.lean
index 037e41c..f4326b7 100644
--- a/Game/Levels/Power/Level_2.lean
+++ b/Game/Levels/Power/Level_2.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Power.Level_1
 
-Game "NNG"
+
 World "Power"
 Level 2
 Title "zero_pow_succ"
diff --git a/Game/Levels/Power/Level_3.lean b/Game/Levels/Power/Level_3.lean
index 10b098a..b227faa 100644
--- a/Game/Levels/Power/Level_3.lean
+++ b/Game/Levels/Power/Level_3.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Power.Level_2
 
-Game "NNG"
+
 World "Power"
 Level 3
 Title "pow_one"
diff --git a/Game/Levels/Power/Level_4.lean b/Game/Levels/Power/Level_4.lean
index c6b7ef0..7ef9b97 100644
--- a/Game/Levels/Power/Level_4.lean
+++ b/Game/Levels/Power/Level_4.lean
@@ -1,7 +1,7 @@
 import Game.Levels.Power.Level_3
 
 
-Game "NNG"
+
 World "Power"
 Level 4
 Title "one_pow"
diff --git a/Game/Levels/Power/Level_5.lean b/Game/Levels/Power/Level_5.lean
index 3f77157..101035f 100644
--- a/Game/Levels/Power/Level_5.lean
+++ b/Game/Levels/Power/Level_5.lean
@@ -1,7 +1,7 @@
 import Game.Levels.Power.Level_4
 
 
-Game "NNG"
+
 World "Power"
 Level 5
 Title "pow_add"
diff --git a/Game/Levels/Power/Level_6.lean b/Game/Levels/Power/Level_6.lean
index a00698e..c7f658a 100644
--- a/Game/Levels/Power/Level_6.lean
+++ b/Game/Levels/Power/Level_6.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Power.Level_5
 
-Game "NNG"
+
 World "Power"
 Level 6
 Title "mul_pow"
diff --git a/Game/Levels/Power/Level_7.lean b/Game/Levels/Power/Level_7.lean
index 9bdbdf6..cbfce83 100644
--- a/Game/Levels/Power/Level_7.lean
+++ b/Game/Levels/Power/Level_7.lean
@@ -1,6 +1,6 @@
 import Game.Levels.Power.Level_6
 
-Game "NNG"
+
 World "Power"
 Level 7
 Title "pow_pow"
diff --git a/Game/Levels/Power/Level_8.lean b/Game/Levels/Power/Level_8.lean
index ae4f2d7..f46c241 100644
--- a/Game/Levels/Power/Level_8.lean
+++ b/Game/Levels/Power/Level_8.lean
@@ -1,7 +1,7 @@
 import Game.Levels.Power.Level_7
 -- import Mathlib.Tactic.Ring
 
-Game "NNG"
+
 World "Power"
 Level 8
 Title "add_squared"
diff --git a/Game/Levels/Proposition.lean b/Game/Levels/Proposition.lean
index e58c8de..4baf164 100644
--- a/Game/Levels/Proposition.lean
+++ b/Game/Levels/Proposition.lean
@@ -9,7 +9,7 @@ import Game.Levels.Proposition.Level_8
 import Game.Levels.Proposition.Level_9 -- `cc` is not ported
 
 
-Game "NNG"
+
 World "Proposition"
 Title "Proposition World"
 
diff --git a/Game/Levels/Proposition/Level_1.lean b/Game/Levels/Proposition/Level_1.lean
index 65f8e5a..14c330d 100644
--- a/Game/Levels/Proposition/Level_1.lean
+++ b/Game/Levels/Proposition/Level_1.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "Proposition"
 Level 1
 Title "the `exact` tactic"
diff --git a/Game/Levels/Proposition/Level_2.lean b/Game/Levels/Proposition/Level_2.lean
index 2f8df41..1639d6f 100644
--- a/Game/Levels/Proposition/Level_2.lean
+++ b/Game/Levels/Proposition/Level_2.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "Proposition"
 Level 2
 Title "intro"
diff --git a/Game/Levels/Proposition/Level_3.lean b/Game/Levels/Proposition/Level_3.lean
index c4ba338..7e981a4 100644
--- a/Game/Levels/Proposition/Level_3.lean
+++ b/Game/Levels/Proposition/Level_3.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "Proposition"
 Level 3
 Title "have"
diff --git a/Game/Levels/Proposition/Level_4.lean b/Game/Levels/Proposition/Level_4.lean
index 6f3c0fe..554b611 100644
--- a/Game/Levels/Proposition/Level_4.lean
+++ b/Game/Levels/Proposition/Level_4.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "Proposition"
 Level 4
 Title "apply"
diff --git a/Game/Levels/Proposition/Level_5.lean b/Game/Levels/Proposition/Level_5.lean
index 419297d..0874611 100644
--- a/Game/Levels/Proposition/Level_5.lean
+++ b/Game/Levels/Proposition/Level_5.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "Proposition"
 Level 5
 Title "P → (Q → P)"
diff --git a/Game/Levels/Proposition/Level_6.lean b/Game/Levels/Proposition/Level_6.lean
index 77ed50c..45b3a48 100644
--- a/Game/Levels/Proposition/Level_6.lean
+++ b/Game/Levels/Proposition/Level_6.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "Proposition"
 Level 6
 Title "(P → (Q → R)) → ((P → Q) → (P → R))"
diff --git a/Game/Levels/Proposition/Level_7.lean b/Game/Levels/Proposition/Level_7.lean
index d8c42f0..d013ab7 100644
--- a/Game/Levels/Proposition/Level_7.lean
+++ b/Game/Levels/Proposition/Level_7.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "Proposition"
 Level 7
 Title "(P → Q) → ((Q → R) → (P → R))"
diff --git a/Game/Levels/Proposition/Level_8.lean b/Game/Levels/Proposition/Level_8.lean
index 88d0dcc..9a31cf8 100644
--- a/Game/Levels/Proposition/Level_8.lean
+++ b/Game/Levels/Proposition/Level_8.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "Proposition"
 Level 8
 Title "(P → Q) → (¬ Q → ¬ P)"
diff --git a/Game/Levels/Proposition/Level_9.lean b/Game/Levels/Proposition/Level_9.lean
index 43de704..044239e 100644
--- a/Game/Levels/Proposition/Level_9.lean
+++ b/Game/Levels/Proposition/Level_9.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "Proposition"
 Level 9
 Title "a big maze."
diff --git a/Game/Levels/Tutorial.lean b/Game/Levels/Tutorial.lean
index a0bf4b8..6acabfa 100644
--- a/Game/Levels/Tutorial.lean
+++ b/Game/Levels/Tutorial.lean
@@ -3,7 +3,7 @@ import Game.Levels.Tutorial.Level_2
 import Game.Levels.Tutorial.Level_3
 import Game.Levels.Tutorial.Level_4
 
-Game "NNG"
+
 World "Tutorial"
 Title "Tutorial World"
 
diff --git a/Game/Levels/Tutorial/Level_1.lean b/Game/Levels/Tutorial/Level_1.lean
index ba28437..d2b028e 100644
--- a/Game/Levels/Tutorial/Level_1.lean
+++ b/Game/Levels/Tutorial/Level_1.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Multiplication
 
-Game "NNG"
+
 World "Tutorial"
 Level 1
 Title "The rfl tactic"
diff --git a/Game/Levels/Tutorial/Level_2.lean b/Game/Levels/Tutorial/Level_2.lean
index eb7b85c..bd3e9b2 100644
--- a/Game/Levels/Tutorial/Level_2.lean
+++ b/Game/Levels/Tutorial/Level_2.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Multiplication
 
-Game "NNG"
+
 World "Tutorial"
 Level 2
 Title "the rw tactic"
diff --git a/Game/Levels/Tutorial/Level_3.lean b/Game/Levels/Tutorial/Level_3.lean
index ed1464c..62f74b5 100644
--- a/Game/Levels/Tutorial/Level_3.lean
+++ b/Game/Levels/Tutorial/Level_3.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Definition
 
-Game "NNG"
+
 World "Tutorial"
 Level 3
 Title "Peano axioms"
diff --git a/Game/Levels/Tutorial/Level_4.lean b/Game/Levels/Tutorial/Level_4.lean
index 52c573e..8a2ddeb 100644
--- a/Game/Levels/Tutorial/Level_4.lean
+++ b/Game/Levels/Tutorial/Level_4.lean
@@ -1,7 +1,7 @@
 import Game.Metadata
 import Game.MyNat.Addition
 
-Game "NNG"
+
 World "Tutorial"
 Level 4
 Title "addition"