diff --git a/Game/Levels/Implication/L03apply.lean b/Game/Levels/Implication/L03apply.lean
index 7068e56..babf455 100644
--- a/Game/Levels/Implication/L03apply.lean
+++ b/Game/Levels/Implication/L03apply.lean
@@ -39,8 +39,11 @@ NewTactic apply
 
 Introduction
 "
-In this level one of our hypotheses is an *implication*. We can use this
-hypothesis with the `apply` tactic.
+In this level, the hypotheses `h2` is an *implication*. It says
+that *if* `x = 37` *then* `y = 42`. We can use this
+hypothesis with the `apply` tactic. Remember you can click on
+`apply` or any other tactic on the right to see a detailed explanation
+of what it does, with examples.
 "
 
 /-- If $x=37$ and we know that $x=37\implies y=42$ then we can deduce $y=42$. -/
diff --git a/Game/Levels/Implication/L07intro2.lean b/Game/Levels/Implication/L07intro2.lean
index 5ddb7c4..fdc4de8 100644
--- a/Game/Levels/Implication/L07intro2.lean
+++ b/Game/Levels/Implication/L07intro2.lean
@@ -16,7 +16,7 @@ Statement (x : ℕ) : x + 1 = y + 1 → x = y := by
   Hint (hidden := true) "Start with `intro h` to assume the hypothesis."
   intro h
   Hint (hidden := true) "Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to
-  change `succ x = succ y`."
+  change `h` to `succ x = succ y`."
   repeat rw [← succ_eq_add_one] at h
   Hint (hidden := true) "Now `apply succ_inj at h` to cancel the `succ`s."
   apply succ_inj at h