diff --git a/README.agda b/README.agda
index 97b8ab3903..ced0f11596 100644
--- a/README.agda
+++ b/README.agda
@@ -237,6 +237,11 @@ import README.Debug.Trace
 
 import README.Nary
 
+-- Explaining the inspect idiom: use case, equivalent handwritten
+-- auxiliary definitions, and implementation details.
+
+import README.Inspect
+
 -- Explaining how to use the automatic solvers
 
 import README.Tactic.MonoidSolver
diff --git a/README/Inspect.agda b/README/Inspect.agda
index 9f40a8d65a..2199a499c8 100644
--- a/README/Inspect.agda
+++ b/README/Inspect.agda
@@ -1,22 +1,19 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- This module is DEPRECATED.
+-- Explaining how to use the inspect idiom and elaborating on the way
+-- it is implemented in the standard library.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
 module README.Inspect where
 
-{-# WARNING_ON_IMPORT
-"README.Inspect was deprecated in v2.0."
-#-}
-
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Product.Base using (_×_; _,_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-open import Relation.Binary.PropositionalEquality using (inspect)
+open import Relation.Binary.PropositionalEquality using (inspect; [_])
 
 ------------------------------------------------------------------------
 -- Using inspect