diff --git a/src/TypedDB.lagda b/src/DeBruijn.lagda
similarity index 100%
rename from src/TypedDB.lagda
rename to src/DeBruijn.lagda
diff --git a/src/TakeDropDec.agda b/src/TakeDropDec.agda
deleted file mode 100644
index 8338126d..00000000
--- a/src/TakeDropDec.agda
+++ /dev/null
@@ -1,43 +0,0 @@
-import Relation.Binary.PropositionalEquality as Eq
-open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
-open import Data.Empty using (⊥; ⊥-elim)
-open import Data.List using (List; []; _∷_)
-open import Data.List.All using (All; []; _∷_)
-open import Data.Bool using (Bool; true; false; T)
-open import Data.Unit using (⊤; tt)
-open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Relation.Nullary.Decidable using ()
-open import Function using (_∘_)
-
-module TakeDropDec2 {A : Set} {P : A → Set} (P? : ∀ (x : A) → Dec (P x)) where
-
-  takeWhile : List A → List A
-  takeWhile []                   =  []
-  takeWhile (x ∷ xs) with P? x
-  ...                   | yes _  =  x ∷ takeWhile xs
-  ...                   | no  _  =  []
-
-  dropWhile : List A → List A
-  dropWhile []                   =  []
-  dropWhile (x ∷ xs) with P? x
-  ...                   | yes _  =  dropWhile xs
-  ...                   | no  _  =  x ∷ xs
-
-  Head : (A → Set) → List A → Set
-  Head P []        =  ⊥
-  Head P (x ∷ xs)  =  P x
-
-  takeWhile-lemma : ∀ (xs : List A) → All P (takeWhile xs)
-  takeWhile-lemma []                    =  []
-  takeWhile-lemma (x ∷ xs) with P? x
-  ...                         | yes px  =  px ∷ takeWhile-lemma xs
-  ...                         | no  _   =  []
-
-  dropWhile-lemma : ∀ (xs : List A) → ¬ Head P (dropWhile xs)
-  dropWhile-lemma []                     =  λ()
-  dropWhile-lemma (x ∷ xs) with P? x
-  ...                         | yes _    =  dropWhile-lemma xs
-  ...                         | no  ¬px  =  ¬px
-
-
-
diff --git a/src/TakeDropDecTest.agda b/src/TakeDropDecTest.agda
index 46bf929f..fee91d50 100644
--- a/src/TakeDropDecTest.agda
+++ b/src/TakeDropDecTest.agda
@@ -5,10 +5,5 @@ open import Data.List using (List; []; _∷_)
 open import Relation.Nullary using (Dec; yes; no)
 open import TakeDropDec2
 
-_ : takeWhile (0 ≟_) (0 ∷ 0 ∷ 1 ∷ []) ≡ (0 ∷ 0 ∷ [])
-_ = refl
-
-_ : dropWhile (0 ≟_) (0 ∷ 0 ∷ 1 ∷ []) ≡ (1 ∷ [])
-_ = refl
 
 
diff --git a/src/extra/TakeDropDec.agda b/src/extra/TakeDropDec.agda
index 264a07bd..859e35d4 100644
--- a/src/extra/TakeDropDec.agda
+++ b/src/extra/TakeDropDec.agda
@@ -1,3 +1,5 @@
+module TakeDropDec where
+
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
 open import Data.Empty using (⊥; ⊥-elim)
@@ -9,35 +11,44 @@ open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Nullary.Decidable using ()
 open import Function using (_∘_)
 
-module TakeDropDec {A : Set} {P : A → Set} where
+module TakeDrop {A : Set} {P : A → Set} (P? : ∀ (x : A) → Dec (P x)) where
 
-Decidable : (A → Set) → Set
-Decidable P = ∀ (x : A) → Dec (P x)
+  takeWhile : List A → List A
+  takeWhile []                   =  []
+  takeWhile (x ∷ xs) with P? x
+  ...                   | yes _  =  x ∷ takeWhile xs
+  ...                   | no  _  =  []
 
-takeWhile : Decidable P → List A → List A
-takeWhile P? []                   =  []
-takeWhile P? (x ∷ xs) with P? x
-...                      | yes _  =  x ∷ takeWhile P? xs
-...                      | no  _  =  []
+  dropWhile : List A → List A
+  dropWhile []                   =  []
+  dropWhile (x ∷ xs) with P? x
+  ...                   | yes _  =  dropWhile xs
+  ...                   | no  _  =  x ∷ xs
 
-dropWhile : Decidable P → List A → List A
-dropWhile P? []                   =  []
-dropWhile P? (x ∷ xs) with P? x
-...                      | yes _  =  dropWhile P? xs
-...                      | no  _  =  x ∷ xs
+  Head : (A → Set) → List A → Set
+  Head P []        =  ⊥
+  Head P (x ∷ xs)  =  P x
+
+  takeWhile-lemma : ∀ (xs : List A) → All P (takeWhile xs)
+  takeWhile-lemma []                    =  []
+  takeWhile-lemma (x ∷ xs) with P? x
+  ...                         | yes px  =  px ∷ takeWhile-lemma xs
+  ...                         | no  _   =  []
+
+  dropWhile-lemma : ∀ (xs : List A) → ¬ Head P (dropWhile xs)
+  dropWhile-lemma []                     =  λ()
+  dropWhile-lemma (x ∷ xs) with P? x
+  ...                         | yes _    =  dropWhile-lemma xs
+  ...                         | no  ¬px  =  ¬px
+
+open TakeDrop
+open import Data.Nat using (ℕ; zero; suc; _≟_)
+
+_ : takeWhile (0 ≟_) (0 ∷ 0 ∷ 1 ∷ []) ≡ (0 ∷ 0 ∷ [])
+_ = refl
+
+_ : dropWhile (0 ≟_) (0 ∷ 0 ∷ 1 ∷ []) ≡ (1 ∷ [])
+_ = refl
 
-Head : (A → Set) → List A → Set
-Head P []        =  ⊥
-Head P (x ∷ xs)  =  P x
 
-takeWhile-lemma : ∀ (P? : Decidable P) (xs : List A) → All P (takeWhile P? xs)
-takeWhile-lemma P? []                    =  []
-takeWhile-lemma P? (x ∷ xs) with P? x
-...                            | yes px  =  px ∷ takeWhile-lemma P? xs
-...                            | no  _   =  []
 
-dropWhile-lemma : ∀ (P? : Decidable P) (xs : List A) → ¬ Head P (dropWhile P? xs)
-dropWhile-lemma P? []                     =  λ()
-dropWhile-lemma P? (x ∷ xs) with P? x
-...                            | yes _    =  dropWhile-lemma P? xs
-...                            | no  ¬px  =  ¬px