diff --git a/src/Collections.lagda b/src/Collections.lagda
index c4968fcc..8467fdb7 100644
--- a/src/Collections.lagda
+++ b/src/Collections.lagda
@@ -24,7 +24,7 @@ open import Data.Empty using (⊥; ⊥-elim)
 open import Isomorphism using (_≃_)
 open import Function using (_∘_)
 open import Level using (Level)
-open import Data.List using (List; []; _∷_; _++_; map; foldr; filter)
+open import Data.List using (List; []; _∷_; [_]; _++_; map; foldr; filter)
 open import Data.List.All using (All; []; _∷_)
 open import Data.List.Any using (Any; here; there)
 open import Data.Maybe using (Maybe; just; nothing)
@@ -49,15 +49,11 @@ module CollectionDec (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
     Coll : Set → Set
     Coll A  =  List A
 
-    [_] : A → Coll A
-    [ x ]  =  x ∷ []
-
     infix 4 _∈_
     infix 4 _⊆_
-    infixl 5 _∪_
     infixl 5 _\\_
 
-    data _∈_ : A → Coll A → Set where
+    data _∈_ : A → List A → Set where
 
       here : ∀ {x xs} →
         ----------
@@ -68,13 +64,10 @@ module CollectionDec (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
         ----------
         w ∈ x ∷ xs
 
-    _⊆_ : Coll A → Coll A → Set
+    _⊆_ : List A → List A → Set
     xs ⊆ ys  =  ∀ {w} → w ∈ xs → w ∈ ys
 
-    _∪_ : Coll A → Coll A → Coll A
-    _∪_ = _++_
-
-    _\\_ : Coll A → A → Coll A
+    _\\_ : List A → A → List A
     xs \\ x  =  filter (¬? ∘ (_≟ x)) xs
 
     refl-⊆ : ∀ {xs} → xs ⊆ xs
@@ -83,83 +76,62 @@ module CollectionDec (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
     trans-⊆ : ∀ {xs ys zs} → xs ⊆ ys → ys ⊆ zs → xs ⊆ zs
     trans-⊆ xs⊆ ys⊆  =  ys⊆ ∘ xs⊆
 
-    lemma-[_] : ∀ {w xs} → w ∈ xs ↔ [ w ] ⊆ xs
-    lemma-[_] = ⟨ forward , backward ⟩
-      where
+    [_]-⊆ : ∀ {x xs} → [ x ] ⊆ x ∷ xs
+    [_]-⊆ here        =  here
+    [_]-⊆ (there ()) 
 
-      forward : ∀ {w xs} → w ∈ xs → [ w ] ⊆ xs
-      forward ∈xs here        =  ∈xs
-      forward ∈xs (there ())
+    lemma₂ : ∀ {w x xs} → x ≢ w → w ∈ x ∷ xs → w ∈ xs
+    lemma₂ x≢  here        =  ⊥-elim (x≢ refl)
+    lemma₂ _   (there w∈)  =  w∈
 
-      backward : ∀ {w xs} → [ w ] ⊆ xs → w ∈ xs
-      backward ⊆xs  =  ⊆xs here
+    there⟨_⟩ : ∀ {w x y xs} → w ∈ xs × w ≢ x → w ∈ y ∷ xs × w ≢ x
+    there⟨ ⟨ w∈ , w≢ ⟩ ⟩  =  ⟨ there w∈ , w≢ ⟩
 
-    lemma-\\-∈-≢ : ∀ {w x xs} → w ∈ xs \\ x ↔ w ∈ xs × w ≢ x
-    lemma-\\-∈-≢ = ⟨ forward , backward ⟩
-      where    
+    \\-to-∈-≢ : ∀ {w x xs} → w ∈ xs \\ x → w ∈ xs × w ≢ x
+    \\-to-∈-≢ {_} {x} {[]}    ()
+    \\-to-∈-≢ {_} {x} {y ∷ _} w∈            with y ≟ x
+    \\-to-∈-≢ {_} {x} {y ∷ _} w∈               | yes refl  =  there⟨ \\-to-∈-≢ w∈ ⟩
+    \\-to-∈-≢ {_} {x} {y ∷ _} here             | no  w≢    =  ⟨ here , w≢ ⟩
+    \\-to-∈-≢ {_} {x} {y ∷ _} (there w∈)       | no  _     =  there⟨ \\-to-∈-≢ w∈ ⟩
 
-      next : ∀ {w x y xs} → w ∈ xs × w ≢ x → w ∈ y ∷ xs × w ≢ x
-      next ⟨ w∈ , w≢ ⟩   =  ⟨ there w∈ , w≢ ⟩
-
-      forward : ∀ {w x xs} → w ∈ xs \\ x → w ∈ xs × w ≢ x
-      forward {_} {x} {[]}    ()
-      forward {_} {x} {y ∷ _} w∈         with y ≟ x
-      forward {_} {x} {y ∷ _} w∈            | yes refl  =  next (forward w∈)
-      forward {_} {x} {y ∷ _} here          | no  y≢    =  ⟨ here , (λ y≡ → y≢ y≡) ⟩
-      forward {_} {x} {y ∷ _} (there w∈)    | no  _     =  next (forward w∈)
-
-      backward : ∀ {w x xs} → w ∈ xs × w ≢ x → w ∈ xs \\ x
-      backward {_} {x} {y ∷ _} ⟨ here     , w≢ ⟩
-                                         with y ≟ x
-      ...                                   | yes refl  =  ⊥-elim (w≢ refl)
-      ...                                   | no  _     =  here
-      backward {_} {x} {y ∷ _} ⟨ there w∈ , w≢ ⟩
-                                         with y ≟ x
-      ...                                  | yes refl   =  backward ⟨ w∈ , w≢ ⟩
-      ...                                  | no  _      =  there (backward ⟨ w∈ , w≢ ⟩)
+    ∈-≢-to-\\ : ∀ {w x xs} → w ∈ xs → w ≢ x → w ∈ xs \\ x
+    ∈-≢-to-\\ {_} {x} {y ∷ _} here       w≢ with y ≟ x
+    ...                                        | yes refl  =  ⊥-elim (w≢ refl)
+    ...                                        | no  _     =  here
+    ∈-≢-to-\\ {_} {x} {y ∷ _} (there w∈) w≢ with y ≟ x
+    ...                                        | yes refl  =  ∈-≢-to-\\ w∈ w≢
+    ...                                        | no  _     =  there (∈-≢-to-\\ w∈ w≢)
 
 
-    lemma-\\-∷ : ∀ {x xs ys} → xs \\ x ⊆ ys ↔ xs ⊆ x ∷ ys
-    lemma-\\-∷ = ⟨ forward , backward ⟩
-      where
+    \\-to-∷ : ∀ {x xs ys} → xs \\ x ⊆ ys → xs ⊆ x ∷ ys
+    \\-to-∷ {x} ⊆ys {w} ∈xs
+         with w ≟ x
+    ...     | yes refl  =  here
+    ...     | no  ≢x    =  there (⊆ys (∈-≢-to-\\ ∈xs ≢x))
 
-      forward : ∀ {x xs ys} → xs \\ x ⊆ ys → xs ⊆ x ∷ ys
-      forward {x} ⊆ys {w} ∈xs
-           with w ≟ x
-      ...     | yes refl  =  here
-      ...     | no  ≢x    =  there (⊆ys (proj₂ lemma-\\-∈-≢ ⟨ ∈xs , ≢x ⟩))
+    ∷-to-\\ : ∀ {x xs ys} → xs ⊆ x ∷ ys → xs \\ x ⊆ ys
+    ∷-to-\\ {x} xs⊆ {w} w∈
+         with \\-to-∈-≢ w∈
+    ...     | ⟨ ∈xs , ≢x ⟩ with w ≟ x
+    ...                       | yes refl                  =  ⊥-elim (≢x refl)
+    ...                       | no  w≢   with (xs⊆ ∈xs)
+    ...                                     | here        =  ⊥-elim (≢x refl)
+    ...                                     | there ∈ys   =  ∈ys
 
-      backward : ∀ {x xs ys} → xs ⊆ x ∷ ys → xs \\ x ⊆ ys
-      backward {x} xs⊆ {w} w∈
-           with proj₁ lemma-\\-∈-≢ w∈
-      ...     | ⟨ ∈xs , ≢x ⟩ with w ≟ x
-      ...                       | yes refl                  =  ⊥-elim (≢x refl)
-      ...                       | no  w≢   with (xs⊆ ∈xs)
-      ...                                     | here        =  ⊥-elim (≢x refl)
-      ...                                     | there ∈ys   =  ∈ys
+    ⊆-++₁ : ∀ {xs ys} → xs ⊆ xs ++ ys
+    ⊆-++₁ here         =  here
+    ⊆-++₁ (there ∈xs)  =  there (⊆-++₁ ∈xs)
 
-    lemma-∪₁ : ∀ {xs ys} → xs ⊆ xs ∪ ys
-    lemma-∪₁ here         =  here
-    lemma-∪₁ (there ∈xs)  =  there (lemma-∪₁ ∈xs)
+    ⊆-++₂ : ∀ {xs ys} → ys ⊆ xs ++ ys
+    ⊆-++₂ {[]}     ∈ys  =  ∈ys
+    ⊆-++₂ {x ∷ xs} ∈ys  =  there (⊆-++₂ {xs} ∈ys)
 
-    lemma-∪₂ : ∀ {xs ys} → ys ⊆ xs ∪ ys
-    lemma-∪₂ {[]}     ∈ys  =  ∈ys
-    lemma-∪₂ {x ∷ xs} ∈ys  =  there (lemma-∪₂ {xs} ∈ys)
-
-    lemma-⊎-∪ : ∀ {w xs ys} → w ∈ xs ⊎ w ∈ ys ↔ w ∈ xs ∪ ys
-    lemma-⊎-∪ = ⟨ forward , backward ⟩
-      where
-
-      forward : ∀ {w xs ys} → w ∈ xs ⊎ w ∈ ys → w ∈ xs ∪ ys
-      forward (inj₁ ∈xs)  =  lemma-∪₁ ∈xs
-      forward (inj₂ ∈ys)  =  lemma-∪₂ ∈ys
-
-      backward : ∀ {xs ys w} → w ∈ xs ∪ ys → w ∈ xs ⊎ w ∈ ys
-      backward {[]}     ∈ys                               =  inj₂ ∈ys
-      backward {x ∷ xs} here                              =  inj₁ here
-      backward {x ∷ xs} (there w∈) with backward {xs} w∈
-      ...                             | inj₁ ∈xs          =  inj₁ (there ∈xs)
-      ...                             | inj₂ ∈ys          =  inj₂ ∈ys
+    ++-to-⊎ : ∀ {xs ys w} → w ∈ xs ++ ys → w ∈ xs ⊎ w ∈ ys
+    ++-to-⊎ {[]}     ∈ys                            =  inj₂ ∈ys
+    ++-to-⊎ {x ∷ xs} here                           =  inj₁ here
+    ++-to-⊎ {x ∷ xs} (there w∈) with ++-to-⊎ {xs} w∈
+    ...                            | inj₁ ∈xs       =  inj₁ (there ∈xs)
+    ...                            | inj₂ ∈ys       =  inj₂ ∈ys
 
 
 \end{code}        
diff --git a/src/Typed.lagda b/src/Typed.lagda
index 97db4a92..48661843 100644
--- a/src/Typed.lagda
+++ b/src/Typed.lagda
@@ -15,7 +15,7 @@ module Typed where
 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; []; _∷_; _++_; map; foldr; filter)
+open import Data.List using (List; []; _∷_; [_]; _++_; map; foldr; filter)
 open import Data.List.Any using (Any; here; there)
 open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≤_; _⊔_; _≟_)
 open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m⊔n; n≤m⊔n; 1+n≰n)
@@ -228,7 +228,7 @@ open Collections.CollectionDec (Id) (_≟_)
 free : Term → List Id
 free (` x)       =  [ x ]
 free (`λ x ⇒ N)  =  free N \\ x
-free (L · M)     =  free L ∪ free M
+free (L · M)     =  free L ++ free M
 \end{code}
 
 ### Fresh identifier
@@ -238,9 +238,8 @@ fresh : List Id → Id
 fresh = foldr _⊔_ 0 ∘ map suc
 
 ⊔-lemma : ∀ {w xs} → w ∈ xs → suc w ≤ fresh xs
-⊔-lemma {w} {x ∷ xs} here         =  m≤m⊔n (suc w) (fresh xs)
-⊔-lemma {w} {x ∷ xs} (there x∈)   =  ≤-trans (⊔-lemma {w} {xs} x∈)
-                                             (n≤m⊔n (suc x) (fresh xs))
+⊔-lemma {_} {_ ∷ xs} here        =  m≤m⊔n _ (fresh xs)
+⊔-lemma {_} {_ ∷ xs} (there x∈)  =  ≤-trans (⊔-lemma x∈) (n≤m⊔n _ (fresh xs))
 
 fresh-lemma : ∀ {x xs} → x ∈ xs → fresh xs ≢ x
 fresh-lemma x∈ refl =  1+n≰n (⊔-lemma x∈)
@@ -271,7 +270,7 @@ subst ys ρ (`λ x ⇒ N)     =  `λ y ⇒ subst (y ∷ ys) (ρ , x ↦ ` y) N
 subst ys ρ (L · M)        =  subst ys ρ L · subst ys ρ M
 
 _[_:=_] : Term → Id → Term → Term
-N [ x := M ]  =  subst (free M ∪ (free N \\ x)) (∅ , x ↦ M) N
+N [ x := M ]  =  subst (free M ++ (free N \\ x)) (∅ , x ↦ M) N
 \end{code}
 
 
@@ -374,8 +373,8 @@ free-lemma : ∀ {Γ M A} → Γ ⊢ M ⦂ A → free M ⊆ dom Γ
 free-lemma (` ⊢x) w∈ with w∈
 ...                     | here          =  dom-lemma ⊢x
 ...                     | there ()   
-free-lemma {Γ} (`λ_ {x = x} {N = N} ⊢N)  =  proj₂ lemma-\\-∷ (free-lemma ⊢N)
-free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈
+free-lemma {Γ} (`λ_ {x = x} {N = N} ⊢N)  =  ∷-to-\\ (free-lemma ⊢N)
+free-lemma (⊢L · ⊢M) w∈ with ++-to-⊎ w∈
 ...                        | inj₁ ∈L    = free-lemma ⊢L ∈L
 ...                        | inj₂ ∈M    = free-lemma ⊢M ∈M
 \end{code}
@@ -387,11 +386,11 @@ free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈
   → (∀ {x A} → x ∈ xs      →  Γ ∋ x ⦂ A  →  Δ ∋ x ⦂ A)
     --------------------------------------------------
   → (∀ {M A} → free M ⊆ xs →  Γ ⊢ M ⦂ A  →  Δ ⊢ M ⦂ A)
-⊢rename ⊢σ ⊆xs (` ⊢x)                =  ` ⊢σ ∈xs ⊢x
+⊢rename ⊢σ ⊆xs (` ⊢x)     =  ` ⊢σ ∈xs ⊢x
   where
-  ∈xs = proj₂ lemma-[_] ⊆xs
+  ∈xs = ⊆xs here
 ⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (`λ_ {x = x} {A = A} {N = N} ⊢N)
-                                     =  `λ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N)
+                          =  `λ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N)
   where
   Γ′   =  Γ , x ⦂ A
   Δ′   =  Δ , x ⦂ A
@@ -404,25 +403,17 @@ free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈
   ...                   | there ∈xs  =  S x≢y (⊢σ ∈xs ⊢y)
 
   ⊆xs′ : free N ⊆ xs′
-  ⊆xs′ = proj₁ lemma-\\-∷ ⊆xs
-⊢rename {xs = xs} ⊢σ {L · M} ⊆xs (⊢L · ⊢M)
-                                     =  ⊢rename ⊢σ L⊆ ⊢L · ⊢rename ⊢σ M⊆ ⊢M
+  ⊆xs′ = \\-to-∷ ⊆xs
+⊢rename ⊢σ ⊆xs (⊢L · ⊢M)  =  ⊢rename ⊢σ L⊆ ⊢L · ⊢rename ⊢σ M⊆ ⊢M
   where
-  L⊆ = trans-⊆ (proj₁ lemma-⊎-∪ ∘ inj₁) ⊆xs
-  M⊆ = trans-⊆ (proj₁ lemma-⊎-∪ ∘ inj₂) ⊆xs
+  L⊆ = trans-⊆ ⊆-++₁ ⊆xs
+  M⊆ = trans-⊆ ⊆-++₂ ⊆xs
 \end{code}
 
 
 ### Substitution preserves types
 
 \begin{code}
-lemma₁ : ∀ {y ys} → [ y ] ⊆ y ∷ ys
-lemma₁ = proj₁ lemma-[_] here
-
-lemma₂ : ∀ {w x xs} → x ≢ w → w ∈ x ∷ xs → w ∈ xs
-lemma₂ x≢  here        =  ⊥-elim (x≢ refl)
-lemma₂ _   (there w∈)  =  w∈
-
 ⊢subst : ∀ {Γ Δ xs ys ρ}
   → (∀ {x}   → x ∈ xs      →  free (ρ x) ⊆ ys)
   → (∀ {x A} → x ∈ xs      →  Γ ∋ x ⦂ A  →  Δ ⊢ ρ x ⦂ A)
@@ -442,33 +433,33 @@ lemma₂ _   (there w∈)  =  w∈
 
   Σ′ : ∀ {w} → w ∈ xs′ →  free (ρ′ w) ⊆ ys′
   Σ′ {w} here         with w ≟ x
-  ...                    | yes refl  =  lemma₁
+  ...                    | yes refl  =  [_]-⊆
   ...                    | no  w≢    =  ⊥-elim (w≢ refl)
   Σ′ {w} (there w∈)   with w ≟ x
-  ...                    | yes refl  =  lemma₁
+  ...                    | yes refl  =  [_]-⊆
   ...                    | no  _     =  there ∘ (Σ w∈)
   
   ⊆xs′ :  free N ⊆ xs′
-  ⊆xs′ =  proj₁ lemma-\\-∷ ⊆xs
+  ⊆xs′ =  \\-to-∷ ⊆xs
 
   ⊢σ : ∀ {w C} → w ∈ ys → Δ ∋ w ⦂ C → Δ′ ∋ w ⦂ C
   ⊢σ w∈ ⊢w  =  S (fresh-lemma w∈) ⊢w
 
   ⊢ρ′ : ∀ {w C} → w ∈ xs′ → Γ′ ∋ w ⦂ C → Δ′ ⊢ ρ′ w ⦂ C
-  ⊢ρ′ _ Z  with x ≟ x
+  ⊢ρ′ {w} Z  with w ≟ x
   ...         | yes _             =  ` Z
-  ...         | no  x≢x           =  ⊥-elim (x≢x refl)
+  ...         | no  w≢x           =  ⊥-elim (w≢x refl)
   ⊢ρ′ {w} w∈′ (S x≢w ⊢w) with w ≟ x
   ...         | yes refl          =  ⊥-elim (x≢w refl)
   ...         | no  _             =  ⊢rename {Δ} {Δ′} {ys} ⊢σ (Σ w∈) (⊢ρ w∈ ⊢w)
               where
               w∈  =  lemma₂ x≢w w∈′ 
 
-⊢subst {xs = xs} Σ ⊢ρ {L · M} ⊆xs (⊢L · ⊢M)
+⊢subst Σ ⊢ρ ⊆xs (⊢L · ⊢M)
     =  ⊢subst Σ ⊢ρ L⊆ ⊢L · ⊢subst Σ ⊢ρ M⊆ ⊢M
   where
-  L⊆ = trans-⊆ lemma-∪₁ ⊆xs
-  M⊆ = trans-⊆ lemma-∪₂ ⊆xs
+  L⊆ = trans-⊆ ⊆-++₁ ⊆xs
+  M⊆ = trans-⊆ ⊆-++₂ ⊆xs
 
 ⊢substitution : ∀ {Γ x A N B M} →
   Γ , x ⦂ A ⊢ N ⦂ B →
@@ -480,15 +471,14 @@ lemma₂ _   (there w∈)  =  w∈
   where
   Γ′     =  Γ , x ⦂ A
   xs     =  free N
-  ys     =  free M ∪ (free N \\ x)
+  ys     =  free M ++ (free N \\ x)
   ρ      =  ∅ , x ↦ M
 
   Σ : ∀ {w} → w ∈ xs → free (ρ w) ⊆ ys
   Σ {w} w∈ y∈ with w ≟ x
-  ...            | yes _                  =  lemma-∪₁ y∈
+  ...            | yes _                  =  ⊆-++₁ y∈
   ...            | no w≢  with y∈
-  ...                        | here       =  lemma-∪₂
-                                                (proj₂ lemma-\\-∈-≢ ⟨ w∈ , w≢ ⟩)
+  ...                        | here       =  ⊆-++₂ (∈-≢-to-\\ w∈ w≢)
   ...                        | there ()   
   
   ⊢ρ : ∀ {z C} → z ∈ xs → Γ′ ∋ z ⦂ C → Γ ⊢ ρ z ⦂ C
diff --git a/src/extra/Typed-backup.lagda b/src/extra/Typed-backup.lagda
index fc16d88f..97db4a92 100644
--- a/src/extra/Typed-backup.lagda
+++ b/src/extra/Typed-backup.lagda
@@ -4,6 +4,7 @@ layout    : page
 permalink : /Typed
 ---
 
+
 ## Imports
 
 \begin{code}
@@ -35,59 +36,60 @@ open import Collections using (_↔_)
 ## Syntax
 
 \begin{code}
-infixr 6 _⇒_
+infixr 5 _⟹_
 infixl 5 _,_⦂_
 infix  4 _∋_⦂_
 infix  4 _⊢_⦂_
-infix  5 ƛ_⦂_⇒_
-infix  5 ƛ_
+infix  5 `λ_⇒_
+infix  5 `λ_
 infixl 6 _·_
+infix  7 `_
 
 Id : Set
 Id = ℕ
 
 data Type : Set where
-  o   : Type
-  _⇒_ : Type → Type → Type
+  `ℕ  : Type
+  _⟹_ : Type → Type → Type
 
 data Env : Set where
   ε     : Env
   _,_⦂_ : Env → Id → Type → Env
 
 data Term : Set where
-  ⌊_⌋      : Id → Term
-  ƛ_⦂_⇒_  : Id → Type → Term → Term
-  _·_     : Term → Term → Term  
+  `_    : Id → Term
+  `λ_⇒_ : Id → Term → Term
+  _·_   : Term → Term → Term  
 
 data _∋_⦂_ : Env → Id → Type → Set where
 
-  Z : ∀ {Γ A x} →
-    -----------------
-    Γ , x ⦂ A ∋ x ⦂ A
+  Z : ∀ {Γ A x}
+      -----------------
+    → Γ , x ⦂ A ∋ x ⦂ A
 
-  S : ∀ {Γ A B x y} →
-    x ≢ y →
-    Γ ∋ y ⦂ B →
-    -----------------
-    Γ , x ⦂ A ∋ y ⦂ B
+  S : ∀ {Γ A B x y}
+    → x ≢ y
+    → Γ ∋ y ⦂ B
+      -----------------
+    → Γ , x ⦂ A ∋ y ⦂ B
 
 data _⊢_⦂_ : Env → Term → Type → Set where
 
-  ⌊_⌋ : ∀ {Γ A x} →
-    Γ ∋ x ⦂ A →
-    ---------------------
-    Γ ⊢ ⌊ x ⌋ ⦂ A
+  `_ : ∀ {Γ A x}
+    → Γ ∋ x ⦂ A
+      ---------------------
+    → Γ ⊢ ` x ⦂ A
 
-  ƛ_ :  ∀ {Γ x A N B} →
-    Γ , x ⦂ A ⊢ N ⦂ B →
-    --------------------------
-    Γ ⊢ (ƛ x ⦂ A ⇒ N) ⦂ A ⇒ B
+  `λ_ : ∀ {Γ x A N B}
+    → Γ , x ⦂ A ⊢ N ⦂ B
+      ------------------------
+    → Γ ⊢ (`λ x ⇒ N) ⦂ A ⟹ B
 
-  _·_ : ∀ {Γ L M A B} →
-    Γ ⊢ L ⦂ A ⇒ B →
-    Γ ⊢ M ⦂ A →
-    --------------
-    Γ ⊢ L · M ⦂ B
+  _·_ : ∀ {Γ L M A B}
+    → Γ ⊢ L ⦂ A ⟹ B
+    → Γ ⊢ M ⦂ A
+      --------------
+    → Γ ⊢ L · M ⦂ B
 \end{code}
 
 ## Test examples
@@ -118,32 +120,31 @@ n≢m : n ≢ m
 n≢m ()
 
 Ch : Type
-Ch = (o ⇒ o) ⇒ o ⇒ o
+Ch = (`ℕ ⟹ `ℕ) ⟹ `ℕ ⟹ `ℕ
 
 two : Term
-two = ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒ (⌊ s ⌋ · (⌊ s ⌋ · ⌊ z ⌋))
+two = `λ s ⇒ `λ z ⇒ (` s · (` s · ` z))
 
 ⊢two : ε ⊢ two ⦂ Ch
-⊢two = ƛ ƛ ⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · ⌊ ⊢z ⌋)
+⊢two = `λ `λ ` ⊢s · (` ⊢s · ` ⊢z)
   where
   ⊢s = S z≢s Z
   ⊢z = Z
 
 four : Term
-four = ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒ ⌊ s ⌋ · (⌊ s ⌋ · (⌊ s ⌋ · (⌊ s ⌋ · ⌊ z ⌋)))
+four = `λ s ⇒ `λ z ⇒ ` s · (` s · (` s · (` s · ` z)))
 
 ⊢four : ε ⊢ four ⦂ Ch
-⊢four = ƛ ƛ ⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · ⌊ ⊢z ⌋)))
+⊢four = `λ `λ ` ⊢s · (` ⊢s · (` ⊢s · (` ⊢s · ` ⊢z)))
   where
   ⊢s = S z≢s Z
   ⊢z = Z
 
 plus : Term
-plus = ƛ m ⦂ Ch ⇒ ƛ n ⦂ Ch ⇒ ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒
-         ⌊ m ⌋ · ⌊ s ⌋ · (⌊ n ⌋ · ⌊ s ⌋ · ⌊ z ⌋)
+plus = `λ m ⇒ `λ n ⇒ `λ s ⇒ `λ z ⇒ ` m · ` s · (` n · ` s · ` z)
 
-⊢plus : ε ⊢ plus ⦂ Ch ⇒ Ch ⇒ Ch
-⊢plus = ƛ ƛ ƛ ƛ  ⌊ ⊢m ⌋ ·  ⌊ ⊢s ⌋ · (⌊ ⊢n ⌋ · ⌊ ⊢s ⌋ · ⌊ ⊢z ⌋)
+⊢plus : ε ⊢ plus ⦂ Ch ⟹ Ch ⟹ Ch
+⊢plus = `λ `λ `λ `λ  ` ⊢m ·  ` ⊢s · (` ⊢n · ` ⊢s · ` ⊢z)
   where
   ⊢z = Z
   ⊢s = S z≢s Z
@@ -162,8 +163,8 @@ four′ = plus · two · two
 
 \begin{code}
 ⟦_⟧ᵀ : Type → Set
-⟦ o ⟧ᵀ      =  ℕ
-⟦ A ⇒ B ⟧ᵀ  =  ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ
+⟦ `ℕ ⟧ᵀ     =  ℕ
+⟦ A ⟹ B ⟧ᵀ  =  ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ
 
 ⟦_⟧ᴱ : Env → Set
 ⟦ ε ⟧ᴱ          =  ⊤
@@ -174,8 +175,8 @@ four′ = plus · two · two
 ⟦ S _ x ⟧ⱽ ⟨ ρ , v ⟩ = ⟦ x ⟧ⱽ ρ
 
 ⟦_⟧ : ∀ {Γ M A} → Γ ⊢ M ⦂ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ
-⟦ ⌊ x ⌋ ⟧   ρ  =  ⟦ x ⟧ⱽ ρ
-⟦ ƛ ⊢N ⟧    ρ  =  λ{ v → ⟦ ⊢N ⟧ ⟨ ρ , v ⟩ }
+⟦ ` x ⟧     ρ  =  ⟦ x ⟧ⱽ ρ
+⟦ `λ ⊢N ⟧   ρ  =  λ{ v → ⟦ ⊢N ⟧ ⟨ ρ , v ⟩ }
 ⟦ ⊢L · ⊢M ⟧ ρ  =  (⟦ ⊢L ⟧ ρ) (⟦ ⊢M ⟧ ρ)
 
 _ : ⟦ ⊢four′ ⟧ tt ≡ ⟦ ⊢four ⟧ tt
@@ -194,22 +195,22 @@ lookup {Γ , x ⦂ A} Z        =  x
 lookup {Γ , x ⦂ A} (S _ k)  =  lookup {Γ} k
 
 erase : ∀ {Γ M A} → Γ ⊢ M ⦂ A → Term
-erase ⌊ k ⌋                     =  ⌊ lookup k ⌋
-erase (ƛ_ {x = x} {A = A} ⊢N)   =  ƛ x ⦂ A ⇒ erase ⊢N
-erase (⊢L · ⊢M)                 =  erase ⊢L · erase ⊢M
+erase (` k)              =  ` lookup k
+erase (`λ_ {x = x} ⊢N)   =  `λ x ⇒ erase ⊢N
+erase (⊢L · ⊢M)          =  erase ⊢L · erase ⊢M
 \end{code}
 
 ### Properties of erasure
 
 \begin{code}
-lookup-lemma : ∀ {Γ x A} → (k : Γ ∋ x ⦂ A) → lookup k ≡ x
+lookup-lemma : ∀ {Γ x A} → (⊢x : Γ ∋ x ⦂ A) → lookup ⊢x ≡ x
 lookup-lemma Z        =  refl
 lookup-lemma (S _ k)  =  lookup-lemma k
 
 erase-lemma : ∀ {Γ M A} → (⊢M : Γ ⊢ M ⦂ A) → erase ⊢M ≡ M
-erase-lemma ⌊ k ⌋                    =  cong ⌊_⌋ (lookup-lemma k)
-erase-lemma (ƛ_ {x = x} {A = A} ⊢N)  =  cong (ƛ x ⦂ A ⇒_) (erase-lemma ⊢N)
-erase-lemma (⊢L · ⊢M)                =  cong₂ _·_ (erase-lemma ⊢L) (erase-lemma ⊢M)
+erase-lemma (` ⊢x)            =  cong `_ (lookup-lemma ⊢x)
+erase-lemma (`λ_ {x = x} ⊢N)  =  cong (`λ x ⇒_) (erase-lemma ⊢N)
+erase-lemma (⊢L · ⊢M)         =  cong₂ _·_ (erase-lemma ⊢L) (erase-lemma ⊢M)
 \end{code}
 
 
@@ -221,39 +222,25 @@ erase-lemma (⊢L · ⊢M)                =  cong₂ _·_ (erase-lemma ⊢L) (er
 open Collections.CollectionDec (Id) (_≟_)
 \end{code}
 
-### Properties of sets
-
-\begin{code}
--- ⊆∷ : ∀ {y xs ys} → xs ⊆ ys → xs ⊆ y ∷ ys
--- ∷⊆∷ : ∀ {x xs ys} → xs ⊆ ys → (x ∷ xs) ⊆ (x ∷ ys)
--- []⊆ : ∀ {x xs} → [ x ] ⊆ xs → x ∈ xs
--- ⊆[] : ∀ {x xs} → x ∈ xs → [ x ] ⊆ xs
--- bind : ∀ {x xs} → xs \\ x ⊆ xs
--- left : ∀ {xs ys} → xs ⊆ xs ∪ ys
--- right : ∀ {xs ys} → ys ⊆ xs ∪ ys
--- prev : ∀ {z y xs} → y ≢ z → z ∈ y ∷ xs → z ∈ xs
-\end{code}
-
 ### Free variables
 
 \begin{code}
 free : Term → List Id
-free ⌊ x ⌋          =  [ x ]
-free (ƛ x ⦂ A ⇒ N)  =  free N \\ x
-free (L · M)        =  free L ∪ free M
+free (` x)       =  [ x ]
+free (`λ x ⇒ N)  =  free N \\ x
+free (L · M)     =  free L ∪ free M
 \end{code}
 
-
 ### Fresh identifier
 
 \begin{code}
 fresh : List Id → Id
 fresh = foldr _⊔_ 0 ∘ map suc
 
-⊔-lemma : ∀ {x xs} → x ∈ xs → suc x ≤ fresh xs
-⊔-lemma {x} {.x ∷ xs} here         =  m≤m⊔n (suc x) (fresh xs)
-⊔-lemma {x} {y  ∷ xs} (there x∈)   =  ≤-trans (⊔-lemma {x} {xs} x∈)
-                                              (n≤m⊔n (suc y) (fresh xs))
+⊔-lemma : ∀ {w xs} → w ∈ xs → suc w ≤ fresh xs
+⊔-lemma {w} {x ∷ xs} here         =  m≤m⊔n (suc w) (fresh xs)
+⊔-lemma {w} {x ∷ xs} (there x∈)   =  ≤-trans (⊔-lemma {w} {xs} x∈)
+                                             (n≤m⊔n (suc x) (fresh xs))
 
 fresh-lemma : ∀ {x xs} → x ∈ xs → fresh xs ≢ x
 fresh-lemma x∈ refl =  1+n≰n (⊔-lemma x∈)
@@ -263,7 +250,9 @@ fresh-lemma x∈ refl =  1+n≰n (⊔-lemma x∈)
 
 \begin{code}
 ∅ : Id → Term
-∅ x = ⌊ x ⌋
+∅ x = ` x
+
+infixl 5 _,_↦_
 
 _,_↦_ : (Id → Term) → Id → Term → (Id → Term)
 (ρ , x ↦ M) w with w ≟ x
@@ -275,8 +264,8 @@ _,_↦_ : (Id → Term) → Id → Term → (Id → Term)
 
 \begin{code}
 subst : List Id → (Id → Term) → Term → Term
-subst ys ρ ⌊ x ⌋          =  ρ x
-subst ys ρ (ƛ x ⦂ A ⇒ N)  =  ƛ y ⦂ A ⇒ subst (y ∷ ys) (ρ , x ↦ ⌊ y ⌋) N
+subst ys ρ (` x)          =  ρ x
+subst ys ρ (`λ x ⇒ N)     =  `λ y ⇒ subst (y ∷ ys) (ρ , x ↦ ` y) N
   where
   y = fresh ys
 subst ys ρ (L · M)        =  subst ys ρ L · subst ys ρ M
@@ -291,74 +280,80 @@ N [ x := M ]  =  subst (free M ∪ (free N \\ x)) (∅ , x ↦ M) N
 \begin{code}
 data Value : Term → Set where
 
-  Fun : ∀ {x A N} →
-    --------------------
-    Value (ƛ x ⦂ A ⇒ N)
+  Fun : ∀ {x N}
+      ---------------
+    → Value (`λ x ⇒ N)
 \end{code}
 
 ## Reduction
 
 \begin{code}
-infix 4 _⟹_
+infix 4 _⟶_
 
-data _⟹_ : Term → Term → Set where
+data _⟶_ : Term → Term → Set where
 
-  β-⇒ : ∀ {x A N V} →
+  β-⟹ : ∀ {x N V}
+    → Value V
+      ------------------------------
+    → (`λ x ⇒ N) · V ⟶ N [ x := V ]
+
+  ξ-⟹₁ : ∀ {L L′ M}
+    → L ⟶ L′
+      ----------------
+    → L · M ⟶ L′ · M
+
+  ξ-⟹₂ : ∀ {V M M′} →
     Value V →
-    ----------------------------------
-    (ƛ x ⦂ A ⇒ N) · V ⟹ N [ x := V ]
-
-  ξ-⇒₁ : ∀ {L L′ M} →
-    L ⟹ L′ →
+    M ⟶ M′ →
     ----------------
-    L · M ⟹ L′ · M
-
-  ξ-⇒₂ : ∀ {V M M′} →
-    Value V →
-    M ⟹ M′ →
-    ----------------
-    V · M ⟹ V · M′
+    V · M ⟶ V · M′
 \end{code}
 
 ## Reflexive and transitive closure
 
 \begin{code}
-infix  2 _⟹*_
+infix  2 _⟶*_
 infix 1 begin_
-infixr 2 _⟹⟨_⟩_
+infixr 2 _⟶⟨_⟩_
 infix 3 _∎
 
-data _⟹*_ : Term → Term → Set where
+data _⟶*_ : Term → Term → Set where
 
-  _∎ : ∀ {M} →
-    -------------
-    M ⟹* M
+  _∎ : ∀ {M}
+      -------------
+    → M ⟶* M
 
-  _⟹⟨_⟩_ : ∀ (L : Term) {M N} →
-    L ⟹ M →
-    M ⟹* N →
-    ---------
-    L ⟹* N
+  _⟶⟨_⟩_ : ∀ (L : Term) {M N}
+    → L ⟶ M
+    → M ⟶* N
+      ---------
+    → L ⟶* N
 
-begin_ : ∀ {M N} → (M ⟹* N) → (M ⟹* N)
-begin M⟹*N = M⟹*N
+begin_ : ∀ {M N} → (M ⟶* N) → (M ⟶* N)
+begin M⟶*N = M⟶*N
 \end{code}
 
 ## Progress
 
 \begin{code}
 data Progress (M : Term) : Set where
-  step : ∀ {N} → M ⟹ N → Progress M
-  done : Value M → Progress M
+  step : ∀ {N}
+    → M ⟶ N
+      ----------
+    → Progress M
+  done :
+      Value M
+      ----------
+    → Progress M
 
 progress : ∀ {M A} → ε ⊢ M ⦂ A → Progress M
-progress ⌊ () ⌋
-progress (ƛ_ ⊢N)                                          =  done Fun
+progress (` ())
+progress (`λ_ ⊢N)                                         =  done Fun
 progress (⊢L · ⊢M) with progress ⊢L
-...                   | step L⟹L′                       =  step (ξ-⇒₁ L⟹L′)
+...                   | step L⟶L′                       =  step (ξ-⟹₁ L⟶L′)
 ...                   | done Fun      with progress ⊢M
-...                                      | step M⟹M′    =  step (ξ-⇒₂ Fun M⟹M′)
-...                                      | done valM      =  step (β-⇒ valM)
+...                                      | step M⟶M′    =  step (ξ-⟹₂ Fun M⟶M′)
+...                                      | done valM      =  step (β-⟹ valM)
 \end{code}
 
 
@@ -376,10 +371,10 @@ dom-lemma Z           =  here
 dom-lemma (S x≢y ⊢y)  =  there (dom-lemma ⊢y)
 
 free-lemma : ∀ {Γ M A} → Γ ⊢ M ⦂ A → free M ⊆ dom Γ
-free-lemma ⌊ ⊢x ⌋ w∈ with w∈
-...                     | here         =  dom-lemma ⊢x
+free-lemma (` ⊢x) w∈ with w∈
+...                     | here          =  dom-lemma ⊢x
 ...                     | there ()   
-free-lemma {Γ} (ƛ_ {x = x} {N = N} ⊢N)  =  proj₂ lemma-\\-∷ (free-lemma ⊢N)
+free-lemma {Γ} (`λ_ {x = x} {N = N} ⊢N)  =  proj₂ lemma-\\-∷ (free-lemma ⊢N)
 free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈
 ...                        | inj₁ ∈L    = free-lemma ⊢L ∈L
 ...                        | inj₂ ∈M    = free-lemma ⊢M ∈M
@@ -388,13 +383,15 @@ free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈
 ### Renaming
 
 \begin{code}
-⊢rename : ∀ {Γ Δ xs} → (∀ {x A} → x ∈ xs      →  Γ ∋ x ⦂ A  →  Δ ∋ x ⦂ A) →
-                       (∀ {M A} → free M ⊆ xs →  Γ ⊢ M ⦂ A  →  Δ ⊢ M ⦂ A)
-⊢rename ⊢σ ⊆xs (⌊ ⊢x ⌋)              =  ⌊ ⊢σ ∈xs ⊢x ⌋
+⊢rename : ∀ {Γ Δ xs}
+  → (∀ {x A} → x ∈ xs      →  Γ ∋ x ⦂ A  →  Δ ∋ x ⦂ A)
+    --------------------------------------------------
+  → (∀ {M A} → free M ⊆ xs →  Γ ⊢ M ⦂ A  →  Δ ⊢ M ⦂ A)
+⊢rename ⊢σ ⊆xs (` ⊢x)                =  ` ⊢σ ∈xs ⊢x
   where
   ∈xs = proj₂ lemma-[_] ⊆xs
-⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (ƛ_ {x = x} {A = A} {N = N} ⊢N)
-                                     =  ƛ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N)
+⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (`λ_ {x = x} {A = A} {N = N} ⊢N)
+                                     =  `λ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N)
   where
   Γ′   =  Γ , x ⦂ A
   Δ′   =  Δ , x ⦂ A
@@ -407,7 +404,7 @@ free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈
   ...                   | there ∈xs  =  S x≢y (⊢σ ∈xs ⊢y)
 
   ⊆xs′ : free N ⊆ xs′
-  ⊆xs′  = proj₁ lemma-\\-∷ ⊆xs
+  ⊆xs′ = proj₁ lemma-\\-∷ ⊆xs
 ⊢rename {xs = xs} ⊢σ {L · M} ⊆xs (⊢L · ⊢M)
                                      =  ⊢rename ⊢σ L⊆ ⊢L · ⊢rename ⊢σ M⊆ ⊢M
   where
@@ -426,21 +423,22 @@ lemma₂ : ∀ {w x xs} → x ≢ w → w ∈ x ∷ xs → w ∈ xs
 lemma₂ x≢  here        =  ⊥-elim (x≢ refl)
 lemma₂ _   (there w∈)  =  w∈
 
-⊢subst : ∀ {Γ Δ xs ys ρ} →
-             (∀ {x}   → x ∈ xs      →  free (ρ x) ⊆ ys) →
-             (∀ {x A} → x ∈ xs      →  Γ ∋ x ⦂ A  →  Δ ⊢ ρ x ⦂ A) →
-             (∀ {M A} → free M ⊆ xs →  Γ ⊢ M ⦂ A  →  Δ ⊢ subst ys ρ M ⦂ A)
-⊢subst Σ ⊢ρ ⊆xs ⌊ ⊢x ⌋
+⊢subst : ∀ {Γ Δ xs ys ρ}
+  → (∀ {x}   → x ∈ xs      →  free (ρ x) ⊆ ys)
+  → (∀ {x A} → x ∈ xs      →  Γ ∋ x ⦂ A  →  Δ ⊢ ρ x ⦂ A)
+    -------------------------------------------------------------
+  → (∀ {M A} → free M ⊆ xs →  Γ ⊢ M ⦂ A  →  Δ ⊢ subst ys ρ M ⦂ A)
+⊢subst Σ ⊢ρ ⊆xs (` ⊢x)
     =  ⊢ρ (⊆xs here) ⊢x
-⊢subst {Γ} {Δ} {xs} {ys} {ρ} Σ ⊢ρ ⊆xs (ƛ_ {x = x} {A = A} {N = N} ⊢N)
-    = ƛ_ {x = y} {A = A} (⊢subst {Γ′} {Δ′} {xs′} {ys′} {ρ′} Σ′ ⊢ρ′ ⊆xs′ ⊢N)
+⊢subst {Γ} {Δ} {xs} {ys} {ρ} Σ ⊢ρ ⊆xs (`λ_ {x = x} {A = A} {N = N} ⊢N)
+    = `λ_ {x = y} {A = A} (⊢subst {Γ′} {Δ′} {xs′} {ys′} {ρ′} Σ′ ⊢ρ′ ⊆xs′ ⊢N)
   where
   y   =  fresh ys
   Γ′  =  Γ , x ⦂ A
   Δ′  =  Δ , y ⦂ A
   xs′ =  x ∷ xs
   ys′ =  y ∷ ys
-  ρ′  =  ρ , x ↦ ⌊ y ⌋
+  ρ′  =  ρ , x ↦ ` y
 
   Σ′ : ∀ {w} → w ∈ xs′ →  free (ρ′ w) ⊆ ys′
   Σ′ {w} here         with w ≟ x
@@ -458,7 +456,7 @@ lemma₂ _   (there w∈)  =  w∈
 
   ⊢ρ′ : ∀ {w C} → w ∈ xs′ → Γ′ ∋ w ⦂ C → Δ′ ⊢ ρ′ w ⦂ C
   ⊢ρ′ _ Z  with x ≟ x
-  ...         | yes _             =  ⌊ Z ⌋
+  ...         | yes _             =  ` Z
   ...         | no  x≢x           =  ⊥-elim (x≢x refl)
   ⊢ρ′ {w} w∈′ (S x≢w ⊢w) with w ≟ x
   ...         | yes refl          =  ⊥-elim (x≢w refl)
@@ -499,7 +497,7 @@ lemma₂ _   (there w∈)  =  w∈
   ...                     | no  x≢x   =  ⊥-elim (x≢x refl)
   ⊢ρ {z} z∈ (S x≢z ⊢z) with z ≟ x
   ...                     | yes refl  =  ⊥-elim (x≢z refl)
-  ...                     | no  _     =  ⌊ ⊢z ⌋
+  ...                     | no  _     =  ` ⊢z
 
   ⊆xs : free N ⊆ xs
   ⊆xs x∈ = x∈
@@ -508,12 +506,16 @@ lemma₂ _   (there w∈)  =  w∈
 ### Preservation
 
 \begin{code}
-preservation : ∀ {Γ M N A} →  Γ ⊢ M ⦂ A  →  M ⟹ N  →  Γ ⊢ N ⦂ A
-preservation ⌊ ⊢x ⌋ ()
-preservation (ƛ ⊢N) ()
-preservation (⊢L · ⊢M) (ξ-⇒₁ L⟹L′)        =  preservation ⊢L L⟹L′ · ⊢M
-preservation (⊢V · ⊢M) (ξ-⇒₂ valV M⟹M′)   =  ⊢V · preservation ⊢M M⟹M′
-preservation ((ƛ ⊢N) · ⊢W) (β-⇒ valW)      =  ⊢substitution ⊢N ⊢W
+preservation : ∀ {Γ M N A}
+  →  Γ ⊢ M ⦂ A
+  →  M ⟶ N
+     ---------
+  →  Γ ⊢ N ⦂ A
+preservation (` ⊢x) ()
+preservation (`λ ⊢N) ()
+preservation (⊢L · ⊢M) (ξ-⟹₁ L⟶L′)        =  preservation ⊢L L⟶L′ · ⊢M
+preservation (⊢V · ⊢M) (ξ-⟹₂ valV M⟶M′)   =  ⊢V · preservation ⊢M M⟶M′
+preservation ((`λ ⊢N) · ⊢W) (β-⟹ valW)      =  ⊢substitution ⊢N ⊢W
 \end{code}