Consistent import of DB

* Re-export test examples from Chapter DeBruijn in Chapter More.

  * In Chapter Inference, as well as Assignment 4, import the
    instrinsically-typed λ-calculus as follows:
      `import plfa.part2.More as DB`

src/plfa/part2/DeBruijn.lagda.md

@@ -449,7 +449,7 @@ _ = ƛ ƛ (# 1 · (# 1 · # 0))
 ```
 
 
-### Test examples
+### Test examples {#examples}
 
 We repeat the test examples from
 Chapter [Lambda]({{ site.baseurl }}/Lambda/).

src/plfa/part2/Inference.lagda.md

@@ -263,7 +263,7 @@ can compare with our previous development, we import
 module `plfa.part2.DeBruijn`:
 
 ```
-import plfa.part2.DeBruijn as DB
+import plfa.part2.More as DB
 ```
 
 The phrase `as DB` allows us to refer to definitions

src/plfa/part2/More.lagda.md

@@ -1232,6 +1232,35 @@ Note the arguments need to be swapped and `W` needs to have
 its context adjusted via renaming in order for the right-hand
 side to be well typed.
 
+## Test examples
+
+We repeat the [test examples]({{ site.baseurl }}/DeBruijn/#examples) from Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn),
+in order to make sure we have not broken anything in the process of extending our base calculus.
+```
+two : ∀ {Γ} → Γ ⊢ `ℕ
+two = `suc `suc `zero
+
+plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
+plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
+
+2+2 : ∀ {Γ} → Γ ⊢ `ℕ
+2+2 = plus · two · two
+
+Ch : Type → Type
+Ch A  =  (A ⇒ A) ⇒ A ⇒ A
+
+twoᶜ : ∀ {Γ A} → Γ ⊢ Ch A
+twoᶜ = ƛ ƛ (# 1 · (# 1 · # 0))
+
+plusᶜ : ∀ {Γ A} → Γ ⊢ Ch A ⇒ Ch A ⇒ Ch A
+plusᶜ = ƛ ƛ ƛ ƛ (# 3 · # 1 · (# 2 · # 1 · # 0))
+
+sucᶜ : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ
+sucᶜ = ƛ `suc (# 0)
+
+2+2ᶜ : ∀ {Γ} → Γ ⊢ `ℕ
+2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
+```
 
 ## Unicode