Fix import in README.Data.Fin.Substitution.UntypedLambda (#2279)

Also import this module in doc/README.agda so that it is covered by CI.

Closes #2278.

Author: andreasabel

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"
 

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; ε; _◅_)