diff --git a/src/Reflection/AST/Abstraction.agda b/src/Reflection/AST/Abstraction.agda
index 4f640bcb20..2f19e5c8b6 100644
--- a/src/Reflection/AST/Abstraction.agda
+++ b/src/Reflection/AST/Abstraction.agda
@@ -8,12 +8,12 @@
 
 module Reflection.AST.Abstraction where
 
-open import Data.String.Base as String                 using (String)
-open import Data.String.Properties as String           using (_≟_)
-open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
+open import Data.String.Base as String using (String)
+open import Data.String.Properties as String using (_≟_)
+open import Data.Product.Base using (_×_; <_,_>; uncurry)
 open import Level using (Level)
-open import Relation.Nullary.Decidable.Core            using (Dec; map′; _×-dec_)
-open import Relation.Binary.Definitions                using (DecidableEquality)
+open import Relation.Nullary.Decidable.Core using (Dec; map′; _×-dec_)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 
 private
diff --git a/src/Reflection/AST/AlphaEquality.agda b/src/Reflection/AST/AlphaEquality.agda
index ec0b556292..fc2e3bfcd5 100644
--- a/src/Reflection/AST/AlphaEquality.agda
+++ b/src/Reflection/AST/AlphaEquality.agda
@@ -8,21 +8,20 @@
 
 module Reflection.AST.AlphaEquality where
 
-open import Data.Bool.Base                   using (Bool; true; false; _∧_)
-open import Data.List.Base                   using ([]; _∷_)
-open import Data.Nat.Base as ℕ               using (ℕ; zero; suc; _≡ᵇ_)
-open import Data.Product.Base                using (_,_)
-open import Relation.Nullary.Decidable.Core  using (⌊_⌋)
-open import Relation.Binary.Definitions      using (DecidableEquality)
-
-open import Reflection.AST.Abstraction
-open import Reflection.AST.Argument
-open import Reflection.AST.Argument.Information as ArgInfo
-open import Reflection.AST.Argument.Modality    as Modality
-open import Reflection.AST.Argument.Visibility  as Visibility
-open import Reflection.AST.Meta                 as Meta
-open import Reflection.AST.Name                 as Name
-open import Reflection.AST.Literal              as Literal
+open import Data.Bool.Base using (Bool; true; false; _∧_)
+open import Data.List.Base using ([]; _∷_)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _≡ᵇ_)
+open import Data.Product.Base using (_,_)
+open import Relation.Nullary.Decidable.Core using (⌊_⌋)
+open import Relation.Binary.Definitions using (DecidableEquality)
+open import Reflection.AST.Abstraction using (Abs; abs)
+open import Reflection.AST.Argument using (Arg; arg; Args)
+open import Reflection.AST.Argument.Information as ArgInfo using (ArgInfo)
+open import Reflection.AST.Argument.Modality as Modality using (Modality)
+open import Reflection.AST.Argument.Visibility as Visibility using (Visibility)
+open import Reflection.AST.Meta as Meta using (Meta)
+open import Reflection.AST.Name as Name using (Name)
+open import Reflection.AST.Literal as Literal using (Literal)
 open import Reflection.AST.Term
 open import Level using (Level)
 
diff --git a/src/Reflection/AST/Argument.agda b/src/Reflection/AST/Argument.agda
index d21b3688cb..2ffc41309f 100644
--- a/src/Reflection/AST/Argument.agda
+++ b/src/Reflection/AST/Argument.agda
@@ -8,13 +8,12 @@
 
 module Reflection.AST.Argument where
 
-open import Data.List.Base as List                     using (List; []; _∷_)
-open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
-open import Relation.Nullary.Decidable.Core            using (Dec; map′; _×-dec_)
-open import Relation.Binary.Definitions                using (DecidableEquality)
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.Product.Base using (_×_; <_,_>; uncurry)
+open import Relation.Nullary.Decidable.Core using (Dec; map′; _×-dec_)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
-open import Level
-
+open import Level using (Level)
 open import Reflection.AST.Argument.Visibility
 open import Reflection.AST.Argument.Relevance
 open import Reflection.AST.Argument.Quantity
diff --git a/src/Reflection/AST/Argument/Information.agda b/src/Reflection/AST/Argument/Information.agda
index 98c91ee818..3aba388215 100644
--- a/src/Reflection/AST/Argument/Information.agda
+++ b/src/Reflection/AST/Argument/Information.agda
@@ -8,11 +8,10 @@
 
 module Reflection.AST.Argument.Information where
 
-open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
-open import Relation.Nullary.Decidable.Core            using (map′; _×-dec_)
-open import Relation.Binary.Definitions                using (DecidableEquality)
+open import Data.Product.Base using (_×_; <_,_>; uncurry)
+open import Relation.Nullary.Decidable.Core using (map′; _×-dec_)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
-
 open import Reflection.AST.Argument.Modality as Modality using (Modality)
 open import Reflection.AST.Argument.Visibility as Visibility using (Visibility)
 
diff --git a/src/Reflection/AST/Argument/Modality.agda b/src/Reflection/AST/Argument/Modality.agda
index 722c1cfa0e..d5f084e5d1 100644
--- a/src/Reflection/AST/Argument/Modality.agda
+++ b/src/Reflection/AST/Argument/Modality.agda
@@ -8,11 +8,10 @@
 
 module Reflection.AST.Argument.Modality where
 
-open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
-open import Relation.Nullary.Decidable.Core            using (map′; _×-dec_)
-open import Relation.Binary.Definitions                using (DecidableEquality)
+open import Data.Product.Base using (_×_; <_,_>; uncurry)
+open import Relation.Nullary.Decidable.Core using (map′; _×-dec_)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
-
 open import Reflection.AST.Argument.Relevance as Relevance using (Relevance)
 open import Reflection.AST.Argument.Quantity as Quantity using (Quantity)
 
diff --git a/src/Reflection/AST/Argument/Quantity.agda b/src/Reflection/AST/Argument/Quantity.agda
index ff0a0d3c65..a042218660 100644
--- a/src/Reflection/AST/Argument/Quantity.agda
+++ b/src/Reflection/AST/Argument/Quantity.agda
@@ -8,8 +8,8 @@
 
 module Reflection.AST.Argument.Quantity where
 
-open import Relation.Nullary.Decidable.Core           using (yes; no)
-open import Relation.Binary.Definitions                using (DecidableEquality)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 ------------------------------------------------------------------------
diff --git a/src/Reflection/AST/Argument/Relevance.agda b/src/Reflection/AST/Argument/Relevance.agda
index b2ef362d7d..a06095dc8b 100644
--- a/src/Reflection/AST/Argument/Relevance.agda
+++ b/src/Reflection/AST/Argument/Relevance.agda
@@ -8,8 +8,8 @@
 
 module Reflection.AST.Argument.Relevance where
 
-open import Relation.Nullary.Decidable.Core            using (yes; no)
-open import Relation.Binary.Definitions                using (DecidableEquality)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 ------------------------------------------------------------------------
diff --git a/src/Reflection/AST/Argument/Visibility.agda b/src/Reflection/AST/Argument/Visibility.agda
index f8bd2afeee..db68cb4b27 100644
--- a/src/Reflection/AST/Argument/Visibility.agda
+++ b/src/Reflection/AST/Argument/Visibility.agda
@@ -8,8 +8,8 @@
 
 module Reflection.AST.Argument.Visibility where
 
-open import Relation.Nullary.Decidable.Core            using (yes; no)
-open import Relation.Binary.Definitions                using (DecidableEquality)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 ------------------------------------------------------------------------
diff --git a/src/Reflection/AST/DeBruijn.agda b/src/Reflection/AST/DeBruijn.agda
index 2973912d3f..ad024b791d 100644
--- a/src/Reflection/AST/DeBruijn.agda
+++ b/src/Reflection/AST/DeBruijn.agda
@@ -8,14 +8,13 @@
 
 module Reflection.AST.DeBruijn where
 
-open import Data.Bool.Base  using (Bool; true; false; _∨_; if_then_else_)
-open import Data.Nat.Base   using (ℕ; zero; suc; _+_; _∸_; _<ᵇ_; _≡ᵇ_)
+open import Data.Bool.Base using (Bool; true; false; _∨_; if_then_else_)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; _∸_; _<ᵇ_; _≡ᵇ_)
 open import Data.List.Base  using (List; []; _∷_; _++_)
 open import Data.Maybe.Base using (Maybe; nothing; just)
-import Data.Maybe.Effectful as Maybe
-import Function.Identity.Effectful as Identity
+import Data.Maybe.Effectful as Maybe using (applicative)
+import Function.Identity.Effectful as Identity using (applicative)
 open import Effect.Applicative using (RawApplicative; mkRawApplicative)
-
 open import Reflection
 open import Reflection.AST.Argument.Visibility using (Visibility)
 import Reflection.AST.Traversal as Traverse
diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda
index 45fc85a00f..1d3f10f1c0 100644
--- a/src/Reflection/AST/Definition.agda
+++ b/src/Reflection/AST/Definition.agda
@@ -8,17 +8,16 @@
 
 module Reflection.AST.Definition where
 
-import Data.List.Properties as List                    using (≡-dec)
-import Data.Nat.Properties as ℕ                        using (_≟_)
-open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
-open import Relation.Nullary.Decidable.Core            using (map′; _×-dec_; yes; no)
-open import Relation.Binary.Definitions                using (DecidableEquality)
+import Data.List.Properties as List using (≡-dec)
+import Data.Nat.Properties as ℕ using (_≟_)
+open import Data.Product.Base using (_×_; <_,_>; uncurry)
+open import Relation.Nullary.Decidable.Core using (map′; _×-dec_; yes; no)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
-
-import Reflection.AST.Argument          as Arg
-import Reflection.AST.Argument.Quantity as Quantity
-import Reflection.AST.Name              as Name
-import Reflection.AST.Term              as Term
+import Reflection.AST.Argument as Arg using (Arg; ≡-dec)
+import Reflection.AST.Argument.Quantity as Quantity using (Quantity; _≟_)
+import Reflection.AST.Name as Name using (Name; _≟_)
+import Reflection.AST.Term as Term using (Term; _≟-Clauses_)
 
 ------------------------------------------------------------------------
 -- Re-exporting type publicly
diff --git a/src/Reflection/AST/Literal.agda b/src/Reflection/AST/Literal.agda
index 540e150169..9048e75ede 100644
--- a/src/Reflection/AST/Literal.agda
+++ b/src/Reflection/AST/Literal.agda
@@ -16,8 +16,8 @@ import Data.String.Properties as String
 import Data.Word64.Properties as Word64
 import Reflection.AST.Meta as Meta
 import Reflection.AST.Name as Name
-open import Relation.Nullary.Decidable.Core            using (yes; no; map′; isYes)
-open import Relation.Binary.Definitions                using (DecidableEquality)
+open import Relation.Nullary.Decidable.Core using (yes; no; map′; isYes)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
 ------------------------------------------------------------------------
diff --git a/src/Reflection/AST/Meta.agda b/src/Reflection/AST/Meta.agda
index a3cac80c9a..bef152149f 100644
--- a/src/Reflection/AST/Meta.agda
+++ b/src/Reflection/AST/Meta.agda
@@ -8,12 +8,12 @@
 
 module Reflection.AST.Meta where
 
-import Data.Nat.Properties as ℕ
-open import Function.Base                              using (_on_)
-open import Relation.Nullary.Decidable.Core            using (map′)
-open import Relation.Binary.Core                       using (Rel)
-open import Relation.Binary.Definitions                using (Decidable; DecidableEquality)
-import Relation.Binary.Construct.On as On
+import Data.Nat.Properties as ℕ using (_≟_)
+open import Function.Base using (_on_)
+open import Relation.Nullary.Decidable.Core using (map′)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Decidable; DecidableEquality)
+import Relation.Binary.Construct.On as On using (decidable)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 
 open import Agda.Builtin.Reflection public
diff --git a/src/Reflection/AST/Name.agda b/src/Reflection/AST/Name.agda
index 5ceb025126..867d14bd6e 100644
--- a/src/Reflection/AST/Name.agda
+++ b/src/Reflection/AST/Name.agda
@@ -8,14 +8,14 @@
 
 module Reflection.AST.Name where
 
-open import Data.List.Base              using (List)
+open import Data.List.Base using (List)
 import Data.Product.Properties as Prodₚ using (≡-dec)
-import Data.Word64.Properties as Wₚ       using (_≟_)
-open import Function.Base               using (_on_)
-open import Relation.Nullary.Decidable.Core            using (map′)
-open import Relation.Binary.Core                       using (Rel)
-open import Relation.Binary.Definitions                using (Decidable; DecidableEquality)
-open import Relation.Binary.Construct.On               using (decidable)
+import Data.Word64.Properties as Wₚ using (_≟_)
+open import Function.Base using (_on_)
+open import Relation.Nullary.Decidable.Core using (map′)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Decidable; DecidableEquality)
+open import Relation.Binary.Construct.On using (decidable)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 
 ------------------------------------------------------------------------
diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda
index 14381c3ba6..2e7ce98b13 100644
--- a/src/Reflection/AST/Term.agda
+++ b/src/Reflection/AST/Term.agda
@@ -8,25 +8,24 @@
 
 module Reflection.AST.Term where
 
-open import Data.List.Base as List                     hiding (_++_)
-open import Data.List.Properties                       using (∷-dec)
-open import Data.Nat.Base                              using (ℕ; zero; suc)
-import Data.Nat.Properties as ℕ
-open import Data.Product.Base                          using (_×_; _,_; <_,_>; uncurry; map₁)
-open import Data.Product.Properties                    using (,-injective)
-open import Data.Maybe.Base                            using (Maybe; just; nothing)
-open import Data.String.Base                           using (String)
-open import Data.String.Properties as String           hiding (_≟_)
-open import Relation.Nullary.Decidable                 using (map′; _×-dec_; yes; no)
-open import Relation.Binary.Definitions                using (Decidable; DecidableEquality)
+open import Data.List.Base as List hiding (_++_)
+open import Data.List.Properties using (∷-dec)
+open import Data.Nat.Base using (ℕ; zero; suc)
+import Data.Nat.Properties as ℕ using (_≟_)
+open import Data.Product.Base using (_×_; _,_; <_,_>; uncurry; map₁)
+open import Data.Product.Properties using (,-injective)
+open import Data.Maybe.Base using (Maybe; just; nothing)
+open import Data.String.Base using (String)
+open import Data.String.Properties as String hiding (_≟_)
+open import Relation.Nullary.Decidable using (map′; _×-dec_; yes; no)
+open import Relation.Binary.Definitions using (Decidable; DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
-
-open import Reflection.AST.Abstraction
-open import Reflection.AST.Argument
+open import Reflection.AST.Abstraction using (Abs; abs; unAbs-dec)
+open import Reflection.AST.Argument as Arg
 open import Reflection.AST.Argument.Information using (visibility)
 open import Reflection.AST.Argument.Visibility as Visibility hiding (_≟_)
-import Reflection.AST.Literal as Literal
-import Reflection.AST.Meta as Meta
+import Reflection.AST.Literal as Literal using (Literal; _≟_)
+import Reflection.AST.Meta as Meta using (Meta; _≟_)
 open import Reflection.AST.Name as Name using (Name)
 
 ------------------------------------------------------------------------
diff --git a/src/Reflection/AST/Traversal.agda b/src/Reflection/AST/Traversal.agda
index 815642bf05..2598b75c1a 100644
--- a/src/Reflection/AST/Traversal.agda
+++ b/src/Reflection/AST/Traversal.agda
@@ -11,12 +11,12 @@ open import Effect.Applicative using (RawApplicative)
 module Reflection.AST.Traversal
   {F : Set → Set} (AppF : RawApplicative F) where
 
-open import Data.Nat.Base     using (ℕ; zero; suc; _+_)
-open import Data.List.Base    using (List; []; _∷_; _++_; reverse; length)
-open import Data.String.Base  using (String)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.List.Base using (List; []; _∷_; _++_; reverse; length)
+open import Data.String.Base using (String)
 open import Data.Product.Base using (_×_; _,_)
-open import Function.Base     using (_∘_)
-open import Reflection        hiding (pure)
+open import Function.Base using (_∘_)
+open import Reflection hiding (pure)
 
 open RawApplicative AppF
 
diff --git a/src/Reflection/AST/Universe.agda b/src/Reflection/AST/Universe.agda
index dac0af71ed..59aad70f58 100644
--- a/src/Reflection/AST/Universe.agda
+++ b/src/Reflection/AST/Universe.agda
@@ -8,12 +8,12 @@
 
 module Reflection.AST.Universe where
 
-open import Data.List.Base             using (List)
-open import Data.String.Base           using (String)
-open import Data.Product.Base          using (_×_)
-open import Reflection.AST.Argument    using (Arg)
+open import Data.List.Base using (List)
+open import Data.String.Base using (String)
+open import Data.Product.Base using (_×_)
+open import Reflection.AST.Argument using (Arg)
 open import Reflection.AST.Abstraction using (Abs)
-open import Reflection.AST.Term        using (Term; Pattern; Sort; Clause)
+open import Reflection.AST.Term using (Term; Pattern; Sort; Clause)
 
 data Univ : Set where
   ⟨term⟩   : Univ
diff --git a/src/Reflection/AnnotatedAST/Free.agda b/src/Reflection/AnnotatedAST/Free.agda
index 2017e2fd9f..90eac1cb0b 100644
--- a/src/Reflection/AnnotatedAST/Free.agda
+++ b/src/Reflection/AnnotatedAST/Free.agda
@@ -8,16 +8,17 @@
 
 module Reflection.AnnotatedAST.Free where
 
-open import Data.Bool.Base               using (if_then_else_)
-open import Data.Nat.Base                using (ℕ; _∸_; compare; _<ᵇ_; less; equal; greater)
-open import Data.List.Base               using (List; []; _∷_; [_]; concatMap; length)
+open import Data.Bool.Base using (if_then_else_)
+open import Data.Nat.Base using (ℕ; _∸_; compare; _<ᵇ_; less; equal; greater)
+open import Data.List.Base using (List; []; _∷_; [_]; concatMap; length)
 open import Data.List.Relation.Unary.All using (_∷_)
-open import Data.Product.Base            using (_×_; _,_; proj₁; proj₂)
-open import Data.String.Base             using (String)
-
-open import Reflection
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.String.Base using (String)
 open import Reflection.AST.Universe
+  using (⟨term⟩; ⟨pat⟩; ⟨clause⟩; ⟨abs⟩; ⟨tel⟩; ⟦_⟧)
 open import Reflection.AnnotatedAST
+  using (Annotated; AnnotationFun; annotate; defaultAnn; ⟨_⟩_; var; absurd
+        ; clause; absurd-clause; abs)
 
 ------------------------------------------------------------------------
 -- Free variable sets as lists of natural numbers