fix typo #44

2023-11-29 12:45:15 +01:00
parent d61fe73466
commit 14f19a4f1b
1 changed files with 1 additions and 1 deletions
--- a/Game/Levels/LessOrEqual/L04le_trans.lean
+++ b/Game/Levels/LessOrEqual/L04le_trans.lean
@@ -23,7 +23,7 @@ and $Q\\implies R$.
 "

 Introduction "
-In this level, we inequalities as *hypotheses*. We have not seen this before.
+In this level, we see inequalities as *hypotheses*. We have not seen this before.
 The `cases` tactic can be used to take `hxy` apart.
 "