Update later.v (#3)

* Update later.v

"forall quantify," to my untrained eye, looks so _wrong_ because I'm used to "forall" being a preposition and "universally" being an adverb. Does this change in the iris world?

* swap 'forall' for 'universally'

---------

Co-authored-by: Simon Gregersen <gregersen@cs.au.dk>

Author: jsalzbergedu

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).

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).