tidied up Typed

src/Collections.lagda

@@ -1,5 +1,5 @@
 ---
-title     : "Collections: Collections represented as Lists"
+title     : "Collections: Representing collections as lists"
 layout    : page
 permalink : /Collections
 ---
@@ -44,9 +44,7 @@ infix 0 _↔_
 _↔_ : Set → Set → Set
 A ↔ B  =  (A → B) × (B → A)
 
-module Collection (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
-
---  abstract
+module CollectionDec (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
 
     Coll : Set → Set
     Coll A  =  List A
@@ -79,11 +77,22 @@ module Collection (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
     _\\_ : Coll A → A → Coll A
     xs \\ x  =  filter (¬? ∘ (_≟ x)) xs
 
-    ⊆-refl : ∀ {xs} → xs ⊆ xs
-    ⊆-refl ∈xs  =  ∈xs
+    refl-⊆ : ∀ {xs} → xs ⊆ xs
+    refl-⊆ ∈xs  =  ∈xs
 
-    ⊆-trans : ∀ {xs ys zs} → xs ⊆ ys → ys ⊆ zs → xs ⊆ zs
-    ⊆-trans xs⊆ ys⊆  =  ys⊆ ∘ xs⊆
+    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
+
+      forward : ∀ {w xs} → w ∈ xs → [ w ] ⊆ xs
+      forward ∈xs here        =  ∈xs
+      forward ∈xs (there ())
+
+      backward : ∀ {w xs} → [ w ] ⊆ xs → w ∈ xs
+      backward ⊆xs  =  ⊆xs here
 
     lemma-\\-∈-≢ : ∀ {w x xs} → w ∈ xs \\ x ↔ w ∈ xs × w ≢ x
     lemma-\\-∈-≢ = ⟨ forward , backward ⟩
@@ -129,32 +138,21 @@ module Collection (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
       ...                                     | here        =  ⊥-elim (≢x refl)
       ...                                     | there ∈ys   =  ∈ys
 
-    lemma₁ : ∀ {w xs} → w ∈ xs ↔ [ w ] ⊆ xs
-    lemma₁ = ⟨ forward , backward ⟩
-      where
+    lemma-∪₁ : ∀ {xs ys} → xs ⊆ xs ∪ ys
+    lemma-∪₁ here         =  here
+    lemma-∪₁ (there ∈xs)  =  there (lemma-∪₁ ∈xs)
 
-      forward : ∀ {w xs} → w ∈ xs → [ w ] ⊆ xs
-      forward ∈xs here        =  ∈xs
-      forward ∈xs (there ())
+    lemma-∪₂ : ∀ {xs ys} → ys ⊆ xs ∪ ys
+    lemma-∪₂ {[]}     ∈ys  =  ∈ys
+    lemma-∪₂ {x ∷ xs} ∈ys  =  there (lemma-∪₂ {xs} ∈ys)
 
-      backward : ∀ {w xs} → [ w ] ⊆ xs → w ∈ xs
-      backward ⊆xs  =  ⊆xs here
-
-    lemma₂ : ∀ {xs ys} → xs ⊆ xs ∪ ys
-    lemma₂ here         =  here
-    lemma₂ (there ∈xs)  =  there (lemma₂ ∈xs)
-
-    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 ⟩
+    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
+      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

src/Typed.lagda

@@ -14,11 +14,12 @@ 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)
-open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
+open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax)
+              renaming (_,_ to ⟨_,_⟩)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Unit using (⊤; tt)
 open import Function using (_∘_)
@@ -27,6 +28,7 @@ open import Function.Equivalence using (_⇔_; equivalence)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Nullary.Negation using (contraposition; ¬?)
 open import Relation.Nullary.Product using (_×-dec_)
+open import Collections using (_↔_)
 \end{code}
 
 
@@ -216,58 +218,20 @@ erase-lemma (⊢L · ⊢M)                =  cong₂ _·_ (erase-lemma ⊢L) (er
 ### Lists as sets
 
 \begin{code}
-infix  4 _∈_
-infix  4 _⊆_
-infixl 5 _∪_
-infixl 5 _\\_
-
-_∈_ : Id → List Id → Set
-x ∈ xs  =  Any (x ≡_) xs
-
-_⊆_ : List Id → List Id → Set
-xs ⊆ ys  =  ∀ {w} → w ∈ xs → w ∈ ys
-
-_∪_ : List Id → List Id → List Id
-xs ∪ ys  =  xs ++ ys
-
-_\\_ : List Id → Id → List Id
-xs \\ x  =  filter (¬? ∘ (x ≟_)) xs
+open Collections.CollectionDec (Id) (_≟_)
 \end{code}
 
 ### Properties of sets
 
 \begin{code}
-⊆∷ : ∀ {y xs ys} → xs ⊆ ys → xs ⊆ y ∷ ys
-⊆∷ xs⊆ ∈xs  =  there (xs⊆ ∈xs)
-
-∷⊆∷ : ∀ {x xs ys} → xs ⊆ ys → (x ∷ xs) ⊆ (x ∷ ys)
-∷⊆∷ xs⊆ (here refl)   =  here refl
-∷⊆∷ xs⊆ (there ∈xs)   =  there (xs⊆ ∈xs)
-
-[]⊆ : ∀ {x xs} → [ x ] ⊆ xs → x ∈ xs
-[]⊆ ⊆xs = ⊆xs (here refl)
-
-⊆[] : ∀ {x xs} → x ∈ xs → [ x ] ⊆ xs
-⊆[] x∈ (here refl) = x∈
-⊆[] x∈ (there ())
-
-bind : ∀ {x xs} → xs \\ x ⊆ xs
-bind {x} {[]} ()
-bind {x} {y ∷ ys} with x ≟ y
-...                   | yes refl  =  ⊆∷  (bind {x} {ys})
-...                   | no  _     =  ∷⊆∷ (bind {x} {ys})
-
-left : ∀ {xs ys} → xs ⊆ xs ∪ ys
-left (here refl)  =  here refl
-left (there x∈)   =  there (left x∈)
-
-right : ∀ {xs ys} → ys ⊆ xs ∪ ys
-right {[]}     y∈  =  y∈
-right {x ∷ xs} y∈  =  there (right {xs} y∈)
-
-prev : ∀ {z y xs} → y ≢ z → z ∈ y ∷ xs → z ∈ xs
-prev y≢z (here z≡y)  =  ⊥-elim (y≢z (sym z≡y))
-prev _   (there z∈)  =  z∈
+-- ⊆∷ : ∀ {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
@@ -287,7 +251,7 @@ fresh : List Id → Id
 fresh = foldr _⊔_ 0 ∘ map suc
 
 ⊔-lemma : ∀ {x xs} → x ∈ xs → suc x ≤ fresh xs
-⊔-lemma {x} {.x ∷ xs} (here refl)  =  m≤m⊔n (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))
 
@@ -302,9 +266,9 @@ fresh-lemma x∈ refl =  1+n≰n (⊔-lemma x∈)
 ∅ x = ⌊ x ⌋
 
 _,_↦_ : (Id → Term) → Id → Term → (Id → Term)
-(ρ , x ↦ M) y with x ≟ y
+(ρ , x ↦ M) w with w ≟ x
 ...               | yes _   =  M
-...               | no  _   =  ρ y
+...               | no  _   =  ρ w
 \end{code}
 
 ### Substitution
@@ -408,85 +372,58 @@ dom ε            =  []
 dom (Γ , x ⦂ A)  =  x ∷ dom Γ
 
 dom-lemma : ∀ {Γ y B} → Γ ∋ y ⦂ B → y ∈ dom Γ
-dom-lemma Z           =  here refl
+dom-lemma Z           =  here
 dom-lemma (S x≢y ⊢y)  =  there (dom-lemma ⊢y)
 
-f : ∀ {x y} → y ∈ [ x ] → y ≡ x
-f (here y≡x)  =  y≡x
-f (there ())
-
-g : ∀ {w xs ys} → w ∈ xs ∪ ys → w ∈ xs ⊎ w ∈ ys
-g {_} {[]}     {ys} w∈  =  inj₂ w∈
-g {_} {x ∷ xs} {ys} (here px)  =  inj₁ (here px)
-g {_} {x ∷ xs} {ys} (there w∈) with g w∈
-...                               | inj₁ ∈xs  =  inj₁ (there ∈xs)
-...                               | inj₂ ∈ys  =  inj₂ ∈ys
-
-k : ∀ {w x xs} → w ∈ xs \\ x → x ≢ w
-k {w} {x} {[]}       ()
-k {w} {x} {x′ ∷ xs′} w∈           with x ≟ x′
-k {w} {x} {x′ ∷ xs′} w∈           | yes refl   =  k {w} {x} {xs′} w∈
-k {w} {x} {x′ ∷ xs′} (here w≡x′)  | no  x≢x′   =  λ x≡w → x≢x′ (trans x≡w w≡x′)
-k {w} {x} {x′ ∷ xs′} (there w∈)   | no  x≢x′   =  k {w} {x} {xs′} w∈
-
-h : ∀ {x xs ys} → xs ⊆ x ∷ ys → xs \\ x ⊆ ys
-h {x} {xs} {ys} xs⊆ {w} w∈ with xs⊆ (bind w∈)
-...                           | here  w≡x      =  ⊥-elim (k {w} {x} {xs} w∈ (sym w≡x))
-...                           | there w∈′      =  w∈′
-
 free-lemma : ∀ {Γ M A} → Γ ⊢ M ⦂ A → free M ⊆ dom Γ
-free-lemma ⌊ ⊢x ⌋ w∈ rewrite f w∈ = dom-lemma ⊢x
-free-lemma {Γ} (ƛ_ {x = x} {N = N} ⊢N)  =  h ih
-  where
-  ih : free N ⊆ x ∷ dom Γ
-  ih = free-lemma ⊢N 
-free-lemma (⊢L · ⊢M) w∈ with g w∈
-...                        | inj₁ ∈L  = free-lemma ⊢L ∈L
-...                        | inj₂ ∈M  = free-lemma ⊢M ∈M
-\end{code}
+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∈
+...                        | inj₁ ∈L    = free-lemma ⊢L ∈L
+...                        | inj₂ ∈M    = free-lemma ⊢M ∈M
 
-Wow! A lot of work to prove stuff that is obvious. Gulp!
+
+-- f : ∀ {x y} → y ∈ [ x ] → y ≡ x
+-- g : ∀ {w xs ys} → w ∈ xs ∪ ys → w ∈ xs ⊎ w ∈ ys
+-- k : ∀ {w x xs} → w ∈ xs \\ x → x ≢ w
+-- h : ∀ {x xs ys} → xs ⊆ x ∷ ys → xs \\ x ⊆ ys
+
+\end{code}
 
 ### Renaming
 
 \begin{code}
-∷drop : ∀ {v vs ys} → v ∷ vs ⊆ ys → vs ⊆ ys
-∷drop ⊆ys ∈vs  =  ⊆ys (there ∈vs)
-
-i : ∀ {w x xs} → w ∈ xs → x ≢ w → w ∈ xs \\ x
-i {w} {x} {.w ∷ xs} (here refl) x≢w with x ≟ w
-...                                    | yes refl  =  ⊥-elim (x≢w refl)
-...                                    | no  _     =  here refl
-i {w} {x} {y ∷ xs}  (there w∈)  x≢w with x ≟ y
-...                                    | yes refl  =  (i {w} {x} {xs} w∈ x≢w)
-...                                    | no  _     =  there (i {w} {x} {xs} w∈ x≢w)
-
-j : ∀ {x xs ys} → xs \\ x ⊆ ys → xs ⊆ x ∷ ys
-j {x} {xs} {ys} ⊆ys {w} w∈ with x ≟ w
-...                           | yes refl  =  here refl
-...                           | no  x≢w   =  there (⊆ys (i w∈ x≢w))
+-- ∷drop : ∀ {v vs ys} → v ∷ vs ⊆ ys → vs ⊆ ys
+-- i : ∀ {w x xs} → w ∈ xs → x ≢ w → w ∈ xs \\ x
+-- j : ∀ {x xs ys} → xs \\ x ⊆ ys → xs ⊆ x ∷ ys
 
 ⊢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 ⌋)              =  ⌊ ⊢σ ∈xs ⊢x ⌋
   where
-  ∈xs = []⊆ ⊆xs
+  ∈xs = proj₂ lemma-[_] ⊆xs
 ⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (ƛ_ {x = x} {A = A} {N = N} ⊢N)
-                                 =  ƛ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N)    -- ⊆xs : free N \\ x ⊆ xs
+                                     =  ƛ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N)
   where
   Γ′   =  Γ , x ⦂ A
   Δ′   =  Δ , x ⦂ A
   xs′  =  x ∷ xs
 
   ⊢σ′ : ∀ {y B} → y ∈ xs′ → Γ′ ∋ y ⦂ B → Δ′ ∋ y ⦂ B
-  ⊢σ′ ∈xs′ Z                      =  Z
-  ⊢σ′ ∈xs′ (S x≢y k) with ∈xs′
-  ...                   | here refl  =  ⊥-elim (x≢y refl)
-  ...                   | there ∈xs  =  S x≢y (⊢σ ∈xs k)
+  ⊢σ′ ∈xs′ Z                         =  Z
+  ⊢σ′ ∈xs′ (S x≢y ⊢y) with ∈xs′
+  ...                   | here       =  ⊥-elim (x≢y refl)
+  ...                   | there ∈xs  =  S x≢y (⊢σ ∈xs ⊢y)
 
   ⊆xs′ : free N ⊆ xs′
-  ⊆xs′  = j ⊆xs
-⊢rename {xs = xs} ⊢σ {L · M} ⊆xs (⊢L · ⊢M)  =  ⊢rename ⊢σ (⊆xs ∘ left) ⊢L · ⊢rename ⊢σ (⊆xs ∘ right) ⊢M
+  ⊆xs′  = proj₁ lemma-\\-∷ ⊆xs
+⊢rename {xs = xs} ⊢σ {L · M} ⊆xs (⊢L · ⊢M)
+                                     =  ⊢rename ⊢σ L⊆ ⊢L · ⊢rename ⊢σ M⊆ ⊢M
+  where
+  L⊆ = trans-⊆ (proj₁ lemma-⊎-∪ ∘ inj₁) ⊆xs
+  M⊆ = trans-⊆ (proj₁ lemma-⊎-∪ ∘ inj₂) ⊆xs
 \end{code}
 
 
@@ -494,20 +431,20 @@ j {x} {xs} {ys} ⊆ys {w} w∈ with x ≟ w
 
 \begin{code}
 lemma₁ : ∀ {y ys} → [ y ] ⊆ y ∷ ys
-lemma₁ (here refl)  =  here refl
-lemma₁ (there ())
+lemma₁ = proj₁ lemma-[_] here
 
-lemma₂ : ∀ {z x xs} → x ≢ z → z ∈ x ∷ xs → z ∈ xs
-lemma₂ x≢z (here refl)   =  ⊥-elim (x≢z refl)
-lemma₂ _   (there z∈xs)  =  z∈xs
+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 ⌋  =  ⊢ρ (⊆xs (here refl)) ⊢x
+⊢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)
+    = ƛ_ {x = y} {A = A} (⊢subst {Γ′} {Δ′} {xs′} {ys′} {ρ′} Σ′ ⊢ρ′ ⊆xs′ ⊢N)
   where
   y   =  fresh ys
   Γ′  =  Γ , x ⦂ A
@@ -516,43 +453,35 @@ lemma₂ _   (there z∈xs)  =  z∈xs
   ys′ =  y ∷ ys
   ρ′  =  ρ , x ↦ ⌊ y ⌋
 
-  Σ′ : ∀ {z} → z ∈ xs′ →  free (ρ′ z) ⊆ ys′
-  Σ′ {z} (here refl)  with x ≟ z
+  Σ′ : ∀ {w} → w ∈ xs′ →  free (ρ′ w) ⊆ ys′
+  Σ′ {w} here         with w ≟ x
   ...                    | yes refl  =  lemma₁
-  ...                    | no  x≢z   =  ⊥-elim (x≢z refl)
-  Σ′ {z} (there x∈)   with x ≟ z
+  ...                    | no  w≢    =  ⊥-elim (w≢ refl)
+  Σ′ {w} (there w∈)   with w ≟ x
   ...                    | yes refl  =  lemma₁
-  ...                    | no  _     =  there ∘ (Σ x∈)
+  ...                    | no  _     =  there ∘ (Σ w∈)
   
   ⊆xs′ :  free N ⊆ xs′
-  ⊆xs′ =  j ⊆xs
-{-
-       free (ƛ x ⦂ A ⇒ N) ⊆ xs
-    =    def'n
-       free N \\ x ⊆ xs
-    =    adjoint
-       free N ⊆ x ∷ xs
--}
+  ⊆xs′ =  proj₁ lemma-\\-∷ ⊆xs
 
-  ⊢σ : ∀ {z C} → z ∈ ys → Δ ∋ z ⦂ C → Δ′ ∋ z ⦂ C
-  ⊢σ z∈ ⊢z  =  S (fresh-lemma z∈) ⊢z
+  ⊢σ : ∀ {w C} → w ∈ ys → Δ ∋ w ⦂ C → Δ′ ∋ w ⦂ C
+  ⊢σ w∈ ⊢w  =  S (fresh-lemma w∈) ⊢w
 
-  ⊢ρ′ : ∀ {z C} → z ∈ xs′ → Γ′ ∋ z ⦂ C → Δ′ ⊢ ρ′ z ⦂ C
+  ⊢ρ′ : ∀ {w C} → w ∈ xs′ → Γ′ ∋ w ⦂ C → Δ′ ⊢ ρ′ w ⦂ C
   ⊢ρ′ _ Z  with x ≟ x
   ...         | yes _             =  ⌊ Z ⌋
   ...         | no  x≢x           =  ⊥-elim (x≢x refl)
-  ⊢ρ′ {z} z∈′ (S x≢z ⊢z) with x ≟ z
-  ...         | yes x≡z           =  ⊥-elim (x≢z x≡z)
-  ...         | no  _             =  ⊢rename {Δ} {Δ′} {ys} ⊢σ (Σ z∈) (⊢ρ z∈ ⊢z)
+  ⊢ρ′ {w} w∈′ (S x≢w ⊢w) with w ≟ x
+  ...         | yes refl          =  ⊥-elim (x≢w refl)
+  ...         | no  _             =  ⊢rename {Δ} {Δ′} {ys} ⊢σ (Σ w∈) (⊢ρ w∈ ⊢w)
               where
-              z∈  =  lemma₂ x≢z z∈′ 
+              w∈  =  lemma₂ x≢w w∈′ 
 
-⊢subst {xs = xs} Σ ⊢ρ {L · M} ⊆xs (⊢L · ⊢M)           =  ⊢subst Σ ⊢ρ L⊆xs ⊢L · ⊢subst Σ ⊢ρ M⊆xs ⊢M
+⊢subst {xs = xs} Σ ⊢ρ {L · M} ⊆xs (⊢L · ⊢M)
+    =  ⊢subst Σ ⊢ρ L⊆ ⊢L · ⊢subst Σ ⊢ρ M⊆ ⊢M
   where
-  L⊆xs  : free L ⊆ xs
-  L⊆xs  =  ⊆xs ∘ left
-  M⊆xs  : free M ⊆ xs
-  M⊆xs  =  ⊆xs ∘ right
+  L⊆ = trans-⊆ (proj₁ lemma-⊎-∪ ∘ inj₁) ⊆xs
+  M⊆ = trans-⊆ (proj₁ lemma-⊎-∪ ∘ inj₂) ⊆xs
 
 ⊢substitution : ∀ {Γ x A N B M} →
   Γ , x ⦂ A ⊢ N ⦂ B →
@@ -568,19 +497,20 @@ lemma₂ _   (there z∈xs)  =  z∈xs
   ρ      =  ∅ , x ↦ M
 
   Σ : ∀ {w} → w ∈ xs → free (ρ w) ⊆ ys
-  Σ {w} w∈ y∈ with x ≟ w
-  ...            | yes _   =  left y∈
-  ...            | no x≢w  with y∈
-  ...                         | here refl  =  right (i {w} {x} {free N} w∈ x≢w)
-  ...                         | there ()   
+  Σ {w} w∈ y∈ with w ≟ x
+  ...            | yes _                  =  lemma-∪₁ y∈
+  ...            | no w≢  with y∈
+  ...                        | here       =  lemma-∪₂
+                                 (proj₂ (lemma-\\-∈-≢ {w} {x} {free N}) ⟨ w∈ , w≢ ⟩)
+  ...                        | there ()   
   
   ⊢ρ : ∀ {z C} → z ∈ xs → Γ′ ∋ z ⦂ C → Γ ⊢ ρ z ⦂ C
   ⊢ρ {.x} z∈ Z         with x ≟ x
   ...                     | yes _     =  ⊢M
   ...                     | no  x≢x   =  ⊥-elim (x≢x refl)
-  ⊢ρ {z} z∈ (S x≢z ⊢z) with x ≟ z
-  ...                     | yes x≡z   =  ⊥-elim (x≢z x≡z)
-  ...                     | no  _     =   ⌊ ⊢z ⌋
+  ⊢ρ {z} z∈ (S x≢z ⊢z) with z ≟ x
+  ...                     | yes refl  =  ⊥-elim (x≢z refl)
+  ...                     | no  _     =  ⌊ ⊢z ⌋
 
   ⊆xs : free N ⊆ xs
   ⊆xs x∈ = x∈