diff --git a/ProofMode.md b/ProofMode.md
index cc19fdf3d8368ba37d0654b94d7e772a3b5c4726..dc14b03b649684b623cf9de8da7a3f9c49b77f53 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -41,7 +41,7 @@ Context management
   the resulting goal.
 - `iPoseProof pm_trm as (x1 ... xn) "ipat"` : put `pm_trm` into the context and
   eliminates it. This tactic is essentially the same as `iDestruct` with the
-  difference that when `pm_trm` is a non-univerisally quantified spatial
+  difference that when `pm_trm` is a non-universally quantified spatial
   hypothesis, it will not throw the hypothesis away.
 - `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the
   hypothesis `P` to the current goal. The specialization pattern `spat`