diff --git a/docs/proof_guide.md b/docs/proof_guide.md
index 59ab9118a9995eb8df709821b4ecb98309d5c7a0..5e4e603488b713b3e55b9088b6e3144a914eecf8 100644
--- a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ -216,7 +216,7 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
 * UR: unital cameras or resources algebras
 * F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
 * G: global camera functor management (typeclass; see the [resource algebra docs](resource_algebras.md))
-* GS: global singleton (a `*G` typeclass withe extra data that needs to be unique in a proof)
+* GS: global singleton (a `*G` type class with extra data that needs to be unique in a proof)
 * GpreS: collecting preconditions to instantiate the corresponding `*GS`
 * I: bunched implication logic (of type `bi`)
 * SI: step-indexed bunched implication logic (of type `sbi`)