diff --git a/tspl/PUC-Assignment2.lagda b/tspl/PUC-Assignment2.lagda
index 4cdd69c5..c9ba962f 100644
--- a/tspl/PUC-Assignment2.lagda
+++ b/tspl/PUC-Assignment2.lagda
@@ -36,6 +36,7 @@ open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
   ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
 open import plfa.Relations using (_<_; z<s; s<s)
 open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+open import Data.Product using (Σ; ∃; Σ-syntax; ∃-syntax)
 open import Data.Unit using (⊤; tt)
 open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
 open import Data.Empty using (⊥; ⊥-elim)
@@ -46,7 +47,9 @@ open import Relation.Nullary.Negation using (¬?)
 open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Nullary.Sum using (_⊎-dec_)
 open import Relation.Nullary.Negation using (contraposition)
-open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
+open import Relation.Unary using (Decidable)
+open import Function using (_∘_)
+open import Level using (Level)
 open import plfa.Relations using (_<_; z<s; s<s)
 open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
 open plfa.Isomorphism.≃-Reasoning