diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx
index 09074097..67c31283 100644
--- a/client/src/components/inventory.tsx
+++ b/client/src/components/inventory.tsx
@@ -229,6 +229,16 @@ export function Documentation() {
     <h1 className="doc">{docTile.displayName}</h1>
     <p><code>{docEntry.data?.statement}</code></p>
     <Markdown>{t(docEntry.data?.content, {ns: gameId})}</Markdown>
+    {/* TODO: The condition below should be updated so that the section
+    is displayed whenever it's non-empty. */}
+    {docTile.proven && <>
+        <h2>Further details</h2>
+        <ul>
+          {docTile.proven && <li>Proven in: <a href={`#/${gameId}/world/${docTile.world}/level/${docTile.level}`}>{docTile.world} level {docTile.level}</a></li>}
+        </ul>
+      </>
+    }
+
   </div>
 }
 
diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
index cbe3f045..831bb914 100644
--- a/server/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -109,7 +109,7 @@ structure InventoryTile where
   hidden := false
   /-- hover text -/
   altTitle : String := default
-deriving ToJson, FromJson, Repr, Inhabited
+deriving ToJson, FromJson, Repr, Inhabited, BEq
 
 def InventoryItem.toTile (item : InventoryItem) : InventoryTile := {
       name := item.name,