fix typo in inequality level 4

Game/Levels/Implication/L04succ_inj.lean

@@ -14,7 +14,7 @@ If `a` and `b` are numbers, then `succ_inj a b` is a proof
 that `succ a = succ b` implies `a = b`. Click on this theorem in the *Peano*
 tab for more information.
 
-Peano had this theorem as an axiom, but in Functional Programming World
+Peano had this theorem as an axiom, but in Algorithm World
 we will show how to prove it in Lean. Right now let's just assume it,
 and let's prove $x+1=4 \\implies x=3$ using it. Again, we will proceed
 by manipulating our hypothesis until it becomes the goal. I will