diff --git a/src/plfa/part1/Quantifiers.lagda.md b/src/plfa/part1/Quantifiers.lagda.md
index 6de734ff..dd160e0c 100644
--- a/src/plfa/part1/Quantifiers.lagda.md
+++ b/src/plfa/part1/Quantifiers.lagda.md
@@ -19,7 +19,7 @@ import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
 open import Relation.Nullary using (¬_)
-open import Data.Product using (_×_; proj₁) renaming (_,_ to ⟨_,_⟩)
+open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
 open import Data.Sum using (_⊎_)
 open import plfa.part1.Isomorphism using (_≃_; extensionality)
 ```