diff --git a/Game/Levels/Implication/L08ne.lean b/Game/Levels/Implication/L08ne.lean
index 271461b..a0b85c0 100644
--- a/Game/Levels/Implication/L08ne.lean
+++ b/Game/Levels/Implication/L08ne.lean
@@ -14,7 +14,7 @@ definition of `≠`. In Lean, `a ≠ b` is *notation* for `a = b → False`.
 Here `False` is a generic false proposition, and `→` is Lean's notation
 for \"implies\". In logic we learn
 that `True → False` is false, but `False → False` is true. Hence
-`X → false` is the logical opposite of `X`.
+`X → False` is the logical opposite of `X`.
 
 Even though `a ≠ b` does not look like an implication,
 you should treat it as an implication. The next two levels will show you how.