typo #30

Game/Levels/Implication/L06intro.lean

@@ -23,7 +23,7 @@ NewTactic intro
 
 
 Introduction
-"We have seen how to `apply` theorems and assumptions of
+"We have seen how to `apply` theorems and assumptions
 of the form `P → Q`. But what if our *goal* is of the form `P → Q`?
 To prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"
 in Lean. We do this with the `intro` tactic.