diff --git a/doc/README.agda b/doc/README.agda
index 41b536a0d0..6a9a3e398c 100644
--- a/doc/README.agda
+++ b/doc/README.agda
@@ -222,6 +222,10 @@ import Text.Printf
 
 import README.Case
 
+-- Showcasing the framework for well-scoped substitutions
+
+import README.Data.Fin.Substitution.UntypedLambda
+
 -- Some examples showing how combinators can be used to emulate
 -- "functional reasoning"
 
diff --git a/doc/README/Data/Fin/Substitution/UntypedLambda.agda b/doc/README/Data/Fin/Substitution/UntypedLambda.agda
index 126959958f..036f7ed5ca 100644
--- a/doc/README/Data/Fin/Substitution/UntypedLambda.agda
+++ b/doc/README/Data/Fin/Substitution/UntypedLambda.agda
@@ -14,7 +14,7 @@ open import Data.Fin.Substitution.Lemmas
 open import Data.Nat.Base hiding (_/_)
 open import Data.Fin.Base using (Fin)
 open import Data.Vec.Base
-open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong; cong₂; module ≡-Reasoning)
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
   using (Star; ε; _◅_)