diff --git a/Game/Levels/Algorithm/L07succ_ne_succ.lean b/Game/Levels/Algorithm/L07succ_ne_succ.lean
index 9682ef5..b261703 100644
--- a/Game/Levels/Algorithm/L07succ_ne_succ.lean
+++ b/Game/Levels/Algorithm/L07succ_ne_succ.lean
@@ -10,20 +10,24 @@ namespace MyNat
 
 Introduction
 "
-Every natural is either `0` or `succ n` for some `n`. Here is an algorithm
-which, given two naturals `a` and `b`, returns the answer to \"does `a = b`?\"
+Here we begin to
+develop an algorithm which, given two naturals `a` and `b`, returns the answer
+to \"does `a = b`?\"
 
-*) If they're both `0`, return \"yes\".
+Here is the algorithm. First note that `a` and `b` are numbers, and hence
+are either `0` or successors.
+
+*) If `a` and `b` are both `0`, return \"yes\".
 
 *) If one is `0` and the other is `succ n`, return \"no\".
 
 *) If `a = succ m` and `b = succ n`, then return the answer to \"does `m = n`?\"
 
-Let's prove that this algorithm always gives the correct answer. The proof that
+Our job now is to *prove* that this algorithm always gives the correct answer. The proof that
 `0 = 0` is `rfl`. The proof that `0 ≠ succ n` is `zero_ne_succ n`, and the proof
 that `succ m ≠ 0` is `succ_ne_zero m`. The proof that if `h : m = n` then
-`succ m = succ n` is `rw [h]` and then `rfl`. The next level is a proof of the one
-remaining case: if `a ≠ b` then `succ a ≠ succ b`.
+`succ m = succ n` is `rw [h]` and then `rfl`. This level is a proof of the one
+remaining job we have to do: if `a ≠ b` then `succ a ≠ succ b`.
 "
 
 TacticDoc contrapose "
diff --git a/Game/Levels/Algorithm/L08decide.lean b/Game/Levels/Algorithm/L08decide.lean
index fe90178..df00b10 100644
--- a/Game/Levels/Algorithm/L08decide.lean
+++ b/Game/Levels/Algorithm/L08decide.lean
@@ -52,7 +52,9 @@ instance instDecidableEq : DecidableEq ℕ
 ```
 
 This Lean code is a formally verified algorithm for deciding equality
-between two naturals. Run it with the `decide` tactic.
+between two naturals. I've typed it in already, behind the scenes.
+Because the algorithm is formally verified to be correct, we can
+use it in Lean proofs. You can run the algorithm with the `decide` tactic.
 "
 
 /-- $20+20=40$. -/