diff --git a/exercises/later.v b/exercises/later.v
index 3957199..0d85dda 100644
--- a/exercises/later.v
+++ b/exercises/later.v
@@ -184,8 +184,8 @@ Proof.
   (**
     The tactic for Löb induction, [iLöb], requires us to specify the
     name of the induction hypothesis, which we here call ["IH"].
-    Optionally, it can also forall quantify any of our variables before
-    performing induction. We here forall quantify [x] as it changes for
+    Optionally, it can also universally quantify over any of our variables
+    before performing induction. We here forall quantify [x] as it changes for
     every recursive call.
   *)
   iLöb as "IH" forall (x).
diff --git a/theories/later.v b/theories/later.v
index 152f7fa..d7e033f 100644
--- a/theories/later.v
+++ b/theories/later.v
@@ -187,8 +187,8 @@ Proof.
   (**
     The tactic for Löb induction, [iLöb], requires us to specify the
     name of the induction hypothesis, which we here call ["IH"].
-    Optionally, it can also forall quantify any of our variables before
-    performing induction. We here forall quantify [x] as it changes for
+    Optionally, it can also universally quantify over any of our variables
+    before performing induction. We here forall quantify [x] as it changes for
     every recursive call.
   *)
   iLöb as "IH" forall (x).