docs(set_theory/game/pgame): Fix note on pgame (#13880)

We never actually quotient by extensionality. What we quotient by is game equivalence.

src/set_theory/game/pgame.lean

@@ -108,7 +108,7 @@ open function
 universes u
 
 /-- The type of pre-games, before we have quotiented
-  by extensionality. In ZFC, a combinatorial game is constructed from
+  by equivalence (`pgame.setoid`). In ZFC, a combinatorial game is constructed from
   two sets of combinatorial games that have been constructed at an earlier
   stage. To do this in type theory, we say that a pre-game is built
   inductively from two families of pre-games indexed over any type