Modify Fin definitions.

4 files changed, 544 insertions, 133 deletions

diff --git a/src/Cfe/Context/Base.agda b/src/Cfe/Context/Base.agda
index e152790..9f3a197 100644
--- a/src/Cfe/Context/Base.agda
+++ b/src/Cfe/Context/Base.agda
@@ -13,7 +13,7 @@ open import Data.Fin.Properties using (toℕ-fromℕ; toℕ-inject₁)
 open import Data.Nat using (ℕ; suc; _∸_; _+_)
 open import Data.Nat.Properties using (+-suc)
 open import Data.Product using (_×_)
-open import Data.Vec using (Vec; []; insert)
+open import Data.Vec using (Vec; []; insert; remove)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise)
 open import Level renaming (suc to lsuc)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; module ≡-Reasoning)
@@ -43,16 +43,25 @@ open Context public
 -- Insertions
 
 wkn₂ : ∀ (ctx : Context n) → Fin< (1+ guard ctx) → Type ℓ ℓ → Context (suc n)
-wkn₂ (Γ,Δ ⊐ g) i τ = insert Γ,Δ (inject<! i) τ ⊐ 1+ g
+wkn₂ (Γ,Δ ⊐ g) i τ = insert Γ,Δ (inject!< i) τ ⊐ 1+ g
 
-wkn₁ : ∀ (ctx : Context n) → Fin> (guard ctx) → Type ℓ ℓ → Context (suc n)
-wkn₁ (Γ,Δ ⊐ g) i τ = insert Γ,Δ (raise> i) τ ⊐ inject₁ g
+wkn₁ : ∀ (ctx : Context n) → Fin> (inject₁ (guard ctx)) → Type ℓ ℓ → Context (suc n)
+wkn₁ (Γ,Δ ⊐ g) i τ = insert Γ,Δ (raise!> i) τ ⊐ inject₁ g
 
 ------------------------------------------------------------------------
 -- Modifications
 
 shift : ∀ (ctx : Context n) → Fin< (1+ guard ctx) → Context n
-shift (Γ,Δ ⊐ _) i = Γ,Δ ⊐ inject<! i
+shift (Γ,Δ ⊐ _) i = Γ,Δ ⊐ inject!< i
+
+------------------------------------------------------------------------
+-- Deletions
+
+remove₂ : ∀ (ctx : Context (suc n)) → Fin< (guard ctx) → Context n
+remove₂ (Γ,Δ ⊐ g) i = remove Γ,Δ (inject!< i) ⊐ predⁱ< i
+
+remove₁ : ∀ (ctx : Context (suc n)) → Fin> (guard ctx) → Context n
+remove₁ (Γ,Δ ⊐ g) i = remove Γ,Δ (raise!> i) ⊐ inject₁ⁱ> i
 
 ------------------------------------------------------------------------
 -- Relations
diff --git a/src/Cfe/Context/Properties.agda b/src/Cfe/Context/Properties.agda
index b718518..569b72e 100644
--- a/src/Cfe/Context/Properties.agda
+++ b/src/Cfe/Context/Properties.agda
@@ -6,7 +6,7 @@ module Cfe.Context.Properties
   {c ℓ} (over : Setoid c ℓ)
   where
 
-open import Cfe.Context.Base over as C
+open import Cfe.Context.Base over
 open import Cfe.Fin
 open import Cfe.Type over using ()
   renaming
@@ -21,7 +21,7 @@ open import Cfe.Type over using ()
   ; ≤-antisym to ≤ᵗ-antisym
   )
 open import Data.Fin hiding (pred; _≟_) renaming (_≤_ to _≤ᶠ_)
-open import Data.Fin.Properties using (toℕ-inject₁; toℕ<n)
+open import Data.Fin.Properties using (toℕ<n; toℕ-injective; toℕ-inject₁)
   renaming
   ( ≤-refl to ≤ᶠ-refl
   ; ≤-reflexive to ≤ᶠ-reflexive
@@ -29,12 +29,17 @@ open import Data.Fin.Properties using (toℕ-inject₁; toℕ<n)
   ; ≤-antisym to ≤ᶠ-antisym
   )
 open import Data.Nat renaming (_≤_ to _≤ⁿ_)
-open import Data.Nat.Properties using (module ≤-Reasoning) renaming (≤-reflexive to ≤ⁿ-reflexive)
+open import Data.Nat.Properties using (<⇒≤pred; pred-mono; module ≤-Reasoning)
+  renaming
+  ( ≤-refl to ≤ⁿ-refl
+  ; ≤-reflexive to ≤ⁿ-reflexive
+  ; ≤-trans to ≤ⁿ-trans
+  )
 open import Data.Product
-open import Data.Vec using ([]; _∷_; Vec; insert)
+open import Data.Vec using ([]; _∷_; Vec; insert; remove)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pw using ([]; _∷_; Pointwise)
 open import Function
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)
+open import Relation.Binary.PropositionalEquality hiding (setoid)
 open import Relation.Nullary.Decidable using (True; toWitness; fromWitness)
 
 private
@@ -52,13 +57,22 @@ private
   pw-antisym antisym (x ∷ xs) (y ∷ ys) = antisym x y ∷ pw-antisym antisym xs ys
 
   pw-insert :
-    ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} {n} {xs : Vec A n} {ys : Vec B n} →
+    ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} {m n} {xs : Vec A m} {ys : Vec B n} →
     ∀ i j {i≡j : True (toℕ i ≟ toℕ j)} {x y} →
     x ∼ y → Pointwise _∼_ xs ys → Pointwise _∼_ (insert xs i x) (insert ys j y)
   pw-insert zero    zero          x xs       = x ∷ xs
   pw-insert (suc i) (suc j) {i≡j} x (y ∷ xs) =
     y ∷ pw-insert i j {i≡j |> toWitness |> cong pred |> fromWitness} x xs
 
+  pw-remove :
+    ∀ {a b ℓ} {A : Set a} {B : Set b} {_∼_ : REL A B ℓ} →
+    ∀ {m n} {xs : Vec A (suc m)} {ys : Vec B (suc n)} →
+    ∀ i j {i≡j : True (toℕ i ≟ toℕ j)} →
+    Pointwise _∼_ xs ys → Pointwise _∼_ (remove xs i) (remove ys j)
+  pw-remove zero zero (_ ∷ xs) = xs
+  pw-remove (suc i) (suc j) {i≡j} (x ∷ y ∷ xs) =
+    x ∷ pw-remove i j {i≡j |> toWitness |> cong pred |> fromWitness} (y ∷ xs)
+
 ------------------------------------------------------------------------
 -- Properties of _≈_
 ------------------------------------------------------------------------
@@ -142,7 +156,6 @@ setoid {n} = record { isEquivalence = ≈-isEquivalence {n} }
 ------------------------------------------------------------------------
 -- Properties of wkn₂
 ------------------------------------------------------------------------
--- Algebraic Properties
 
 wkn₂-mono :
   ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} {τ₁ τ₂} →
@@ -150,8 +163,8 @@ wkn₂-mono :
 wkn₂-mono i j {i≡j} τ₁≤τ₂ (g₂≤g₁ , Γ,Δ₁≤Γ,Δ₂) =
   s≤s g₂≤g₁ ,
   pw-insert
-    (inject<! i) (inject<! j)
-    {i≡j |> toWitness |> inject<!-cong |> cong toℕ |> fromWitness}
+    (inject!< i) (inject!< j)
+    {i≡j |> toWitness |> inject!<-cong |> fromWitness}
     τ₁≤τ₂
     Γ,Δ₁≤Γ,Δ₂
 
@@ -166,17 +179,22 @@ wkn₂-cong i j {i≡j} τ₁≈τ₂ ctx₁≈ctx₂ =
       (≤ᵗ-reflexive (≈ᵗ-sym τ₁≈τ₂))
       (≤-reflexive (≈-sym ctx₁≈ctx₂)))
 
+wkn₂-cong-≡ :
+  ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} {τ₁ τ₂} →
+  τ₁ ≡ τ₂ → ctx₁ ≡ ctx₂ → wkn₂ {n} ctx₁ i τ₁ ≡ wkn₂ ctx₂ j τ₂
+wkn₂-cong-≡ {ctx₁ = Γ,Δ ⊐ g} i j {i≡j} {τ} refl refl =
+  i≡j |> toWitness |> inject!<-cong |> toℕ-injective |> cong (λ x → insert Γ,Δ x τ ⊐ suc g)
+
 wkn₂-comm :
   ∀ ctx i j τ τ′ →
-  wkn₂ (wkn₂ {n} ctx (inject<!′ {j = suc i} j) τ′) (suc i) τ ≈ wkn₂ (wkn₂ ctx i τ) (inject<′ j) τ′
-wkn₂-comm (Γ,Δ ⊐ g)          i      zero     τ τ′ = ≈-refl
+  wkn₂ (wkn₂ {n} ctx (inject!<< {j = suc i} j) τ′) (suc i) τ ≡ wkn₂ (wkn₂ ctx i τ) (inject<< j) τ′
+wkn₂-comm (Γ,Δ ⊐ g)         i       zero    τ τ′ = refl
 wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) (suc j) τ τ′ =
-  wkn₂-cong zero zero ≈ᵗ-refl (wkn₂-comm (Γ,Δ ⊐ g) i j τ τ′)
+  wkn₂-cong-≡ zero zero refl (wkn₂-comm (Γ,Δ ⊐ g) i j τ τ′)
 
 ------------------------------------------------------------------------
 -- Properties of wkn₁
 ------------------------------------------------------------------------
--- Algebraic Properties
 
 wkn₁-mono :
   ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} →
@@ -188,15 +206,15 @@ wkn₁-mono {_} {_ ⊐ g₁} {_ ⊐ g₂} i j {i≡j} τ₁≤τ₂ (g₂≤g₁
     toℕ g₁           ≡˘⟨ toℕ-inject₁ g₁ ⟩
     toℕ (inject₁ g₁) ∎) ,
   pw-insert
-    (raise> i) (raise> j)
-    {i≡j |> toWitness |> raise>-cong |> cong toℕ |> fromWitness}
+    (raise!> i) (raise!> j)
+    {i≡j |> toWitness |> raise!>-cong |> fromWitness}
     τ₁≤τ₂
     Γ,Δ₁≤Γ,Δ₂
   where open ≤-Reasoning
 
 wkn₁-cong :
-  ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} →
-  ∀ {τ₁ τ₂} → τ₁ ≈ᵗ τ₂ → ctx₁ ≈ ctx₂ → wkn₁ {n} ctx₁ i τ₁ ≈ wkn₁ ctx₂ j τ₂
+  ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} {τ₁ τ₂} →
+  τ₁ ≈ᵗ τ₂ → ctx₁ ≈ ctx₂ → wkn₁ {n} ctx₁ i τ₁ ≈ wkn₁ ctx₂ j τ₂
 wkn₁-cong i j {i≡j} τ₁≈τ₂ ctx₁≈ctx₂ =
   ≤-antisym
     (wkn₁-mono i j {i≡j} (≤ᵗ-reflexive τ₁≈τ₂) (≤-reflexive ctx₁≈ctx₂))
@@ -205,40 +223,38 @@ wkn₁-cong i j {i≡j} τ₁≈τ₂ ctx₁≈ctx₂ =
       (≤ᵗ-reflexive (≈ᵗ-sym τ₁≈τ₂))
       (≤-reflexive (≈-sym ctx₁≈ctx₂)))
 
+wkn₁-cong-≡ :
+  ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} {τ₁ τ₂} →
+  τ₁ ≡ τ₂ → ctx₁ ≡ ctx₂ → wkn₁ {n} ctx₁ i τ₁ ≡ wkn₁ ctx₂ j τ₂
+wkn₁-cong-≡ {ctx₁ = Γ,Δ ⊐ g} i j {i≡j} {τ} refl refl =
+  i≡j |> toWitness |> raise!>-cong |> toℕ-injective |> cong (λ x → insert Γ,Δ x τ ⊐ inject₁ g)
+
 wkn₁-comm :
   ∀ ctx i j τ τ′ →
-  let g = guard ctx in
-  wkn₁ (wkn₁ {n} ctx (inject>!′ {j = suc> i} j) τ′) (suc> i) τ ≈ wkn₁ (wkn₁ ctx i τ) (inject>′ j) τ′
--- wkn₁-comm = {!!}
-wkn₁-comm (Γ,Δ ⊐ zero)      zero    zero    τ τ′ = ≈-refl
+  wkn₁ (wkn₁ {n} ctx (inject!>< {j = suc> i} j) τ′) (suc> i) τ ≡ wkn₁ (wkn₁ ctx i τ) (inject>< j) τ′
+wkn₁-comm (Γ,Δ ⊐ zero)      zero    zero    τ τ′ = refl
 wkn₁-comm (Γ,Δ ⊐ zero)      (suc i) zero    τ τ′ =
-  wkn₁-cong zero zero ≈ᵗ-refl
-    (wkn₁-cong (suc> i) (suc i) {toℕ>-suc> i |> fromWitness } ≈ᵗ-refl ≈-refl)
+  wkn₁-cong-≡ zero zero refl
+    (wkn₁-cong-≡ (suc> i) (suc i) {toℕ-suc> i |> fromWitness } refl refl)
 wkn₁-comm (_ ∷ Γ,Δ ⊐ zero)  (suc i) (suc j) τ τ′ =
-  wkn₁-cong zero zero ≈ᵗ-refl (wkn₁-comm (Γ,Δ ⊐ zero) i j τ τ′)
+  wkn₁-cong-≡ zero zero refl (wkn₁-comm (Γ,Δ ⊐ zero) i j τ τ′)
 wkn₁-comm (_ ∷ Γ,Δ ⊐ suc g) (inj i) (inj j) τ τ′ =
-  wkn₂-cong zero zero ≈ᵗ-refl (wkn₁-comm (Γ,Δ ⊐ g) i j τ τ′)
+  wkn₂-cong-≡ zero zero refl (wkn₁-comm (Γ,Δ ⊐ g) i j τ τ′)
 
 wkn₁-wkn₂-comm :
   ∀ ctx i j τ τ′ →
-  wkn₁ (wkn₂ {n} ctx j τ′) (inj i) τ ≈ wkn₂ (wkn₁ ctx i τ) (cast<-inject₁ j) τ′
-wkn₁-wkn₂-comm (Γ,Δ ⊐ g)         i       zero    τ τ′ = ≈-refl
+  wkn₁ (wkn₂ {n} ctx j τ′) (inj i) τ ≡
+  wkn₂ (wkn₁ ctx i τ) (cast< (guard ctx |> toℕ-inject₁ |> cong suc |> sym) j) τ′
+wkn₁-wkn₂-comm (Γ,Δ ⊐ g)         i       zero    τ τ′ = refl
 wkn₁-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (inj i) (suc j) τ τ′ =
-  wkn₂-cong zero zero ≈ᵗ-refl (wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i j τ τ′)
+  wkn₂-cong-≡ zero zero refl (wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i j τ τ′)
 
 ------------------------------------------------------------------------
 -- Properties of shift
 ------------------------------------------------------------------------
 
 shift-mono : ∀ {ctx₁ ctx₂ i j} → toℕ< j ≤ⁿ toℕ< i → ctx₁ ≤ ctx₂ → shift {n} ctx₁ i ≤ shift ctx₂ j
-shift-mono {i = i} {j} j≤i (_ , Γ,Δ₁≤Γ,Δ₂) =
-  (begin
-    toℕ (inject<! j) ≡⟨ toℕ<-inject<! j ⟩
-    toℕ< j           ≤⟨ j≤i ⟩
-    toℕ< i           ≡˘⟨ toℕ<-inject<! i ⟩
-    toℕ (inject<! i) ∎) ,
-  Γ,Δ₁≤Γ,Δ₂
-  where open ≤-Reasoning
+shift-mono {i = i} {j} j≤i (_ , Γ,Δ₁≤Γ,Δ₂) = inject!<-mono j≤i , Γ,Δ₁≤Γ,Δ₂
 
 shift-cong :
   ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} → ctx₁ ≈ ctx₂ → shift {n} ctx₁ i ≈ shift ctx₂ j
@@ -247,35 +263,157 @@ shift-cong i j {i≡j} ctx₁≈ctx₂ =
     (shift-mono (i≡j |> toWitness |> sym |> ≤ⁿ-reflexive) (≤-reflexive ctx₁≈ctx₂))
     (shift-mono (i≡j |> toWitness |> ≤ⁿ-reflexive) (≤-reflexive (≈-sym ctx₁≈ctx₂)))
 
-shift-identity : ∀ ctx → shift {n} ctx (strengthen< (guard ctx)) ≈ ctx
-shift-identity (Γ,Δ ⊐ zero)       = ≈-refl
-shift-identity (_ ∷ Γ,Δ ⊐ suc g) = wkn₂-cong zero zero ≈ᵗ-refl (shift-identity (Γ,Δ ⊐ g))
+shift-cong-≡ :
+  ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} → ctx₁ ≡ ctx₂ → shift {n} ctx₁ i ≡ shift ctx₂ j
+shift-cong-≡ {ctx₁ = Γ,Δ ⊐ _} i j {i≡j} refl =
+  i≡j |> toWitness |> inject!<-cong |> toℕ-injective |> cong (Γ,Δ ⊐_)
 
-shift-trans : ∀ ctx i j → shift (shift {n} ctx i) (inject<!′-inject! j) ≈ shift {n} ctx (inject<!′ j)
-shift-trans (Γ,Δ ⊐ _)         _       zero    = ≈-refl
+shift-identity : ∀ ctx → shift {n} ctx (strengthen< (guard ctx)) ≡ ctx
+shift-identity (Γ,Δ ⊐ zero)       = refl
+shift-identity (_ ∷ Γ,Δ ⊐ suc g) = wkn₂-cong-≡ zero zero refl (shift-identity (Γ,Δ ⊐ g))
+
+shift-trans :
+  ∀ ctx i j →
+  shift (shift {n} ctx i) (inject!<< (cast<< (strengthen<-inject!< i |> cong suc |> sym) j)) ≡
+  shift ctx (inject!<< j)
+shift-trans (Γ,Δ ⊐ _)         _       zero    = refl
 shift-trans (_ ∷ Γ,Δ ⊐ suc g) (suc i) (suc j) =
-  wkn₂-cong zero zero ≈ᵗ-refl (shift-trans (Γ,Δ ⊐ g) i j)
+  wkn₂-cong-≡ zero zero refl (shift-trans (Γ,Δ ⊐ g) i j)
 
 shift-wkn₁-comm :
   ∀ ctx i j τ →
-  shift (wkn₁ {n} ctx j τ) (cast<-inject₁ i) ≈ wkn₁ (shift ctx i) (cast>-inject<! i j) τ
+  let i≤g = ≤ⁿ-trans (≤ⁿ-reflexive (toℕ-inject!< i)) (pred-mono (toℕ<<i i)) in
+  shift (wkn₁ {n} ctx j τ) (cast< (toℕ-inject₁ (guard ctx) |> cong suc |> sym) i) ≡
+  wkn₁ (shift ctx i) (cast> (inject₁-mono i≤g) j) τ
 shift-wkn₁-comm (Γ,Δ ⊐ zero)      zero    j τ =
-  wkn₁-cong j (cast>-inject<! zero j) {toℕ>-cast>-inject<! zero j |> fromWitness} ≈ᵗ-refl ≈-refl
+ wkn₁-cong-≡ j (cast> ≤ⁿ-refl j) {toℕ-cast> ≤ⁿ-refl j |> sym |> fromWitness} refl refl
 shift-wkn₁-comm (_ ∷ Γ,Δ ⊐ suc g) zero    (inj j) τ =
-  wkn₁-cong zero zero ≈ᵗ-refl (shift-wkn₁-comm (Γ,Δ ⊐ g) zero j τ)
+  wkn₁-cong-≡ zero zero refl (shift-wkn₁-comm (Γ,Δ ⊐ g) zero j τ)
 shift-wkn₁-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) (inj j) τ =
-  wkn₂-cong zero zero ≈ᵗ-refl (shift-wkn₁-comm (Γ,Δ ⊐ g) i j τ)
+  wkn₂-cong-≡ zero zero refl (shift-wkn₁-comm (Γ,Δ ⊐ g) i j τ)
 
 shift-wkn₂-comm :
   ∀ ctx i j τ →
-  shift (wkn₂ {n} ctx (inject<!′ j) τ) (suc i) ≈ wkn₂ (shift ctx i) (inject<!′-inject! j) τ
-shift-wkn₂-comm (Γ,Δ ⊐ g)         i       zero    τ = ≈-refl
+  shift (wkn₂ {n} ctx (inject!<< j) τ) (suc i) ≡
+  wkn₂ (shift ctx i) (inject!<< (cast<< (strengthen<-inject!< i |> cong suc |> sym) j)) τ
+shift-wkn₂-comm (Γ,Δ ⊐ g)         i       zero    τ = refl
 shift-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) (suc j) τ =
-  wkn₂-cong zero zero ≈ᵗ-refl (shift-wkn₂-comm (Γ,Δ ⊐ g) i j τ)
+  wkn₂-cong-≡ zero zero refl (shift-wkn₂-comm (Γ,Δ ⊐ g) i j τ)
 
 shift-wkn₁-wkn₂-comm :
   ∀ ctx i j τ →
-  shift (wkn₂ {n} ctx i τ) (inject<′ j) ≈ wkn₁ (shift ctx (inject<!′ j)) (reflect i j) τ
-shift-wkn₁-wkn₂-comm (Γ,Δ ⊐ g) zero zero τ = ≈-refl
-shift-wkn₁-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) zero τ = wkn₁-cong zero zero ≈ᵗ-refl (shift-wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i zero τ)
-shift-wkn₁-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) (suc j) τ = wkn₂-cong zero zero ≈ᵗ-refl (shift-wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i j τ)
+  shift (wkn₂ {n} ctx i τ) (inject<< j) ≡ wkn₁ (shift ctx (inject!<< j)) (reflect! i j) τ
+shift-wkn₁-wkn₂-comm (Γ,Δ ⊐ g)         zero    zero    τ = refl
+shift-wkn₁-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) zero    τ =
+  wkn₁-cong-≡ zero zero refl (shift-wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i zero τ)
+shift-wkn₁-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g) (suc i) (suc j) τ =
+  wkn₂-cong-≡ zero zero refl (shift-wkn₁-wkn₂-comm (Γ,Δ ⊐ g) i j τ)
+
+------------------------------------------------------------------------
+-- Properties of remove₂
+------------------------------------------------------------------------
+
+remove₂-mono :
+  ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} →
+  ctx₁ ≤ ctx₂ → remove₂ {n} ctx₁ i ≤ remove₂ ctx₂ j
+remove₂-mono i j {i≡j} (g₂≤g₁ , Γ,Δ₁≤Γ,Δ₂) =
+  predⁱ<-mono j i g₂≤g₁ ,
+  pw-remove (inject!< i) (inject!< j) {i≡j |> toWitness |> inject!<-cong |> fromWitness} Γ,Δ₁≤Γ,Δ₂
+
+remove₂-cong :
+  ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} →
+  ctx₁ ≈ ctx₂ → remove₂ {n} ctx₁ i ≈ remove₂ ctx₂ j
+remove₂-cong i j {i≡j} ctx₁≈ctx₂ =
+  ≤-antisym
+    (remove₂-mono i j {i≡j} (≤-reflexive ctx₁≈ctx₂))
+    (remove₂-mono j i {i≡j |> toWitness |> sym |> fromWitness} (≤-reflexive (≈-sym ctx₁≈ctx₂)))
+
+remove₂-cong-≡ :
+  ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} →
+  ctx₁ ≡ ctx₂ → remove₂ {n} ctx₁ i ≡ remove₂ ctx₂ j
+remove₂-cong-≡ {ctx₁ = Γ,Δ ⊐ _} i j {i≡j} refl =
+  i≡j |> toWitness |> λ i≡j →
+    cong₂
+      _⊐_
+      (i≡j |> inject!<-cong |> toℕ-injective |> cong (remove Γ,Δ))
+      (predⁱ<-cong i j refl |> toℕ-injective)
+
+remove₂-wkn₂-comm :
+  ∀ ctx i j τ →
+  remove₂ (wkn₂ {suc n} ctx (inject<< {j = suc i} j) τ) (suc i) ≡
+  wkn₂ (remove₂ ctx i) (cast< (sym (toℕ-predⁱ< i)) (inject!<< j)) τ
+remove₂-wkn₂-comm (_ ∷ Γ,Δ ⊐ suc g)            i       zero          τ = refl
+remove₂-wkn₂-comm (_ ∷ τ′ ∷ Γ,Δ ⊐ suc (suc g)) (suc i) (suc zero)    τ = refl
+remove₂-wkn₂-comm (_ ∷ τ′ ∷ Γ,Δ ⊐ suc (suc g)) (suc i) (suc (suc j)) τ =
+  wkn₂-cong-≡ zero zero refl (remove₂-wkn₂-comm (τ′ ∷ Γ,Δ ⊐ suc g) i (suc j) τ)
+
+------------------------------------------------------------------------
+-- Properties of remove₁
+------------------------------------------------------------------------
+
+remove₁-mono :
+  ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} →
+  ctx₁ ≤ ctx₂ → remove₁ {n} ctx₁ i ≤ remove₁ ctx₂ j
+remove₁-mono i j {i≡j} (g₂≤g₁ , Γ,Δ₁≤Γ,Δ₂) =
+  inject₁ⁱ>-mono j i g₂≤g₁ ,
+  pw-remove (raise!> i) (raise!> j) {i≡j |> toWitness |> raise!>-cong |> fromWitness} Γ,Δ₁≤Γ,Δ₂
+
+remove₁-cong :
+  ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} →
+  ctx₁ ≈ ctx₂ → remove₁ {n} ctx₁ i ≈ remove₁ ctx₂ j
+remove₁-cong i j {i≡j} ctx₁≈ctx₂ =
+  ≤-antisym
+    (remove₁-mono i j {i≡j} (≤-reflexive ctx₁≈ctx₂))
+    (remove₁-mono j i {i≡j |> toWitness |> sym |> fromWitness} (≤-reflexive (≈-sym ctx₁≈ctx₂)))
+
+remove₁-cong-≡ :
+  ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} →
+  ctx₁ ≡ ctx₂ → remove₁ {n} ctx₁ i ≡ remove₁ ctx₂ j
+remove₁-cong-≡ {ctx₁ = Γ,Δ ⊐ _} i j {i≡j} refl =
+  i≡j |> toWitness |> λ i≡j →
+    cong₂
+      _⊐_
+      (i≡j |> raise!>-cong |> toℕ-injective |> cong (remove Γ,Δ))
+      (inject₁ⁱ>-cong i j refl |> toℕ-injective)
+
+remove₁-wkn₂-comm :
+  ∀ ctx i j τ →
+  remove₁ (wkn₂ {suc n} ctx j τ) (inj i) ≡
+  wkn₂ (remove₁ ctx i) (cast< (toℕ-inject₁ⁱ> i |> cong suc |> sym) j) τ
+remove₁-wkn₂-comm (_ ∷ Γ,Δ ⊐ g)               _       zero           τ = refl
+remove₁-wkn₂-comm (_ ∷ _ ∷ Γ,Δ ⊐ suc zero)    (inj i) (suc zero)     τ = refl
+remove₁-wkn₂-comm (_ ∷ _ ∷ Γ,Δ ⊐ suc (suc g)) (inj i) (suc zero)     τ = refl
+remove₁-wkn₂-comm (_ ∷ τ′ ∷ Γ,Δ ⊐ suc (suc g)) (inj i) (suc (suc j)) τ =
+  wkn₂-cong-≡ zero zero refl (remove₁-wkn₂-comm ((τ′ ∷ Γ,Δ) ⊐ suc g) i (suc j) τ)
+
+remove₁-shift-comm :
+  ∀ ctx i j →
+  remove₁ (shift ctx i) (cast> (≤ⁿ-trans (≤ⁿ-reflexive (toℕ-inject!< i)) (<⇒≤pred (toℕ<<i i))) j) ≡
+  shift (remove₁ {n} ctx j) (cast< (toℕ-inject₁ⁱ> j |> cong suc |> sym) i)
+remove₁-shift-comm (Γ,Δ ⊐ g)                    zero    zero    = refl
+remove₁-shift-comm (Γ,Δ ⊐ g)                    zero    (suc j) =
+  toℕ-cast> z≤n j |> raise!>-cong |> toℕ-injective |> cong ((_⊐ zero) ∘ remove Γ,Δ ∘ suc)
+remove₁-shift-comm (Γ,Δ ⊐ g)                    zero    (inj j) =
+  toℕ-cast> z≤n j |> raise!>-cong |> toℕ-injective |> cong ((_⊐ zero) ∘ remove Γ,Δ ∘ suc)
+remove₁-shift-comm (_ ∷ τ′ ∷ Γ,Δ ⊐ suc zero)    (suc i) (inj j) =
+  wkn₂-cong-≡ zero zero refl (remove₁-shift-comm (τ′ ∷ Γ,Δ ⊐ zero) i j)
+remove₁-shift-comm (_ ∷ τ′ ∷ Γ,Δ ⊐ suc (suc g)) (suc i) (inj j) =
+  wkn₂-cong-≡ zero zero refl (remove₁-shift-comm (τ′ ∷ Γ,Δ ⊐ suc g) i j)
+
+-- remove₁ (shift ctx zero) (reflect i zero) ≡ shift (remove ctx i) zero
+remove₁-remove₂-shift-comm :
+  ∀ ctx i j →
+  let eq = inject-square j |> cong toℕ |> sym |> ≤ⁿ-reflexive in
+  remove₁ (shift {suc n} ctx (inject<< j)) (cast> eq (reflect i j)) ≡
+  shift (remove₂ ctx i) (cast< (sym (toℕ-predⁱ< i)) (inject!<< j))
+remove₁-remove₂-shift-comm (Γ,Δ ⊐ suc g)                zero    zero    = refl
+remove₁-remove₂-shift-comm (Γ,Δ ⊐ suc (suc g))          (suc i) zero    =
+  cong ((_⊐ zero) ∘ remove Γ,Δ ∘ suc) (toℕ-injective (begin
+    toℕ (raise!> (cast> _ (reflect i zero))) ≡⟨ toℕ-raise!> (cast> _ (reflect i zero)) ⟩
+    toℕ> (cast> _ (reflect i zero))          ≡⟨ toℕ-cast> z≤n (reflect i zero) ⟩
+    toℕ> (reflect i zero)                    ≡⟨ toℕ-reflect i zero ⟩
+    toℕ< i                                   ≡˘⟨ toℕ-inject!< i ⟩
+    toℕ (inject!< i)                         ∎))
+  where open ≡-Reasoning
+remove₁-remove₂-shift-comm (_ ∷ τ′ ∷ Γ,Δ ⊐ suc (suc g)) (suc i) (suc j) =
+  wkn₂-cong-≡ zero zero refl (remove₁-remove₂-shift-comm (τ′ ∷ Γ,Δ ⊐ suc g) i j)
diff --git a/src/Cfe/Fin/Base.agda b/src/Cfe/Fin/Base.agda
index 9a0a4aa..f357048 100644
--- a/src/Cfe/Fin/Base.agda
+++ b/src/Cfe/Fin/Base.agda
@@ -2,29 +2,33 @@
 
 module Cfe.Fin.Base where
 
-open import Data.Nat using (ℕ; zero; suc)
-open import Data.Fin using (Fin; Fin′; zero; suc; inject₁)
+open import Data.Empty using (⊥-elim)
+open import Data.Nat using (ℕ; zero; suc; pred; z≤n)
+open import Data.Nat.Properties using (pred-mono)
+open import Data.Fin using (Fin; zero; suc; toℕ; inject₁; _≤_)
+open import Function using (_∘_)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong)
 
 data Fin< : ∀ {n} → Fin n → Set where
   zero : ∀ {n i} → Fin< {suc n} (suc i)
   suc  : ∀ {n i} → Fin< {n} i → Fin< (suc i)
 
-data Fin<′ : ∀ {n i} → Fin< {n} i → Set where
-  zero : ∀ {n i j} → Fin<′ {suc n} {suc i} (suc j)
-  suc  : ∀ {n i j} → Fin<′ {n} {i} j → Fin<′ (suc j)
-
--- Fin> {n} zero    ≡ Fin n
--- Fin>     (suc i) ≡ Fin> i
+data Fin<< : ∀ {n i} → Fin< {n} i → Set where
+  zero : ∀ {n i j} → Fin<< {suc n} {suc i} (suc j)
+  suc  : ∀ {n i j} → Fin<< {n} {i} j → Fin<< (suc j)
 
 data Fin> : ∀ {n} → Fin n → Set where
-  zero : ∀ {n} → Fin> {suc n} zero
+  zero : ∀ {n} → Fin> {suc (suc n)} zero
   suc  : ∀ {n} → Fin> {suc n} zero → Fin> {suc (suc n)} zero
   inj  : ∀ {n i} → Fin> {n} i → Fin> (suc i)
 
-data Fin>′ : ∀ {n i} → Fin> {n} i → Set where
-  zero : ∀ {n j} → Fin>′ {suc (suc n)} {zero} (suc j)
-  suc  : ∀ {n j} → Fin>′ {suc n} {zero} j → Fin>′ (suc j)
-  inj  : ∀ {n i j} → Fin>′ {n} {i} j → Fin>′ (inj j)
+data Fin>< : ∀ {n i} → Fin> {n} i → Set where
+  zero : ∀ {n j} → Fin>< {suc (suc n)} {zero} (suc j)
+  suc  : ∀ {n j} → Fin>< {suc n} {zero} j → Fin>< (suc j)
+  inj  : ∀ {n i j} → Fin>< {n} {i} j → Fin>< (inj j)
+
+------------------------------------------------------------------------
+-- Coversions to ℕ
 
 toℕ< : ∀ {n i} → Fin< {n} i → ℕ
 toℕ< zero    = 0
@@ -35,58 +39,118 @@ toℕ> zero    = 0
 toℕ> (suc j) = suc (toℕ> j)
 toℕ> (inj j) = suc (toℕ> j)
 
+------------------------------------------------------------------------
+-- Upwards injections
+
+inject!< : ∀ {n i} → Fin< {suc n} i → Fin n
+inject!< {suc _} zero    = zero
+inject!< {suc _} (suc j) = suc (inject!< j)
+
+inject< : ∀ {n i} → Fin< {n} i → Fin n
+inject< zero    = zero
+inject< (suc j) = suc (inject< j)
+
+inject₁< : ∀ {n i} → Fin< {n} i → Fin< (suc i)
+inject₁< zero    = zero
+inject₁< (suc j) = suc (inject₁< j)
+
+inject!<< : ∀ {n i j} → Fin<< {suc n} {suc i} j → Fin< i
+inject!<< {suc _} {suc _} zero    = zero
+inject!<< {suc _} {suc _} (suc k) = suc (inject!<< k)
+
+inject<< : ∀ {n i j} → Fin<< {n} {i} j → Fin< i
+inject<< zero    = zero
+inject<< (suc k) = suc (inject<< k)
+
+inject!>< : ∀ {n i j} → Fin>< {suc n} {inject₁ i} j → Fin> i
+inject!>< {suc (suc _)} {zero}  {suc j}  zero    = zero
+inject!>< {suc (suc _)} {zero}  {suc j}  (suc k) = suc (inject!>< k)
+inject!>< {suc (suc _)} {suc _} {inj j}  (inj k) = inj (inject!>< k)
+
+inject>< : ∀ {n i j} → Fin>< {n} {i} j → Fin> {n} i
+inject>< zero    = zero
+inject>< (suc k) = suc (inject>< k)
+inject>< (inj k) = inj (inject>< k)
+
+------------------------------------------------------------------------
+-- Downwards injections
+
 strengthen< : ∀ {n} → (i : Fin n) → Fin< (suc i)
 strengthen< zero    = zero
 strengthen< (suc i) = suc (strengthen< i)
 
-inject<! : ∀ {n i} → Fin< {suc n} i → Fin n
-inject<! {suc _} zero    = zero
-inject<! {suc _} (suc j) = suc (inject<! j)
+------------------------------------------------------------------------
+-- Casts
 
-cast<-inject₁ : ∀ {n i} → Fin< {n} i → Fin< (inject₁ i)
-cast<-inject₁ zero    = zero
-cast<-inject₁ (suc j) = suc (cast<-inject₁ j)
+cast< : ∀ {m n i j} → .(toℕ i ≡ toℕ j) → Fin< {m} i → Fin< {n} j
+cast< {i = suc _} {suc _} _   zero    = zero
+cast< {i = suc _} {suc _} i≡j (suc k) = suc (cast< (cong pred i≡j) k)
 
-inject<!′ : ∀ {n i j} → Fin<′ {suc n} {suc i} j → Fin< i
-inject<!′ {suc _} {suc _} zero    = zero
-inject<!′ {suc _} {suc _} (suc k) = suc (inject<!′ k)
+cast<< : ∀ {m n i j k l} → .(toℕ< k ≡ toℕ< l) → Fin<< {m} {i} k → Fin<< {n} {j} l
+cast<< {k = suc _} {suc _} _   zero    = zero
+cast<< {k = suc _} {suc _} k≡l (suc x) = suc (cast<< (cong pred k≡l) x)
 
-inject<′ : ∀ {n i j} → Fin<′ {n} {i} j → Fin< i
-inject<′ zero    = zero
-inject<′ (suc k) = suc (inject<′ k)
+cast> : ∀ {n i j} → .(j ≤ i) → Fin> {n} i → Fin> j
+cast> {_}           {zero}  {zero}  j≤i zero    = zero
+cast> {_}           {zero}  {zero}  j≤i (suc k) = suc (cast> j≤i k)
+cast> {suc (suc _)} {suc i} {zero}  j≤i (inj k) = suc (cast> z≤n k)
+cast> {suc (suc _)} {suc i} {suc j} j≤i (inj k) = inj (cast> (pred-mono j≤i) k)
 
-inject<!′-inject! : ∀ {n i j} → Fin<′ {suc n} {i} j → Fin< (inject<! j)
-inject<!′-inject! {suc n} {_} {suc j} zero    = zero
-inject<!′-inject! {suc n} {_} {suc j} (suc k) = suc (inject<!′-inject! k)
+------------------------------------------------------------------------
+-- Additions
 
-raise> : ∀ {n i} → Fin> {n} i → Fin n
-raise> {suc _} zero    = zero
-raise> {suc _} (suc j) = suc (raise> j)
-raise> {suc _} (inj j) = suc (raise> j)
+raise!> : ∀ {n i} → Fin> {suc n} i → Fin n
+raise!> {suc _} zero    = zero
+raise!> {suc _} (suc j) = suc (raise!> j)
+raise!> {suc _} (inj j) = suc (raise!> j)
 
 suc> : ∀ {n i} → Fin> {n} i → Fin> (inject₁ i)
 suc> zero    = suc zero
 suc> (suc j) = suc (suc> j)
 suc> (inj j) = inj (suc> j)
 
-inject>!′ : ∀ {n i j} → Fin>′ {suc n} {inject₁ i} j → Fin> {n} i
-inject>!′ {suc _}       {zero}          zero    = zero
-inject>!′ {suc (suc _)} {zero}  {suc _} (suc k) = suc (inject>!′ k)
-inject>!′ {suc _}       {suc i}         (inj k) = inj (inject>!′ k)
+------------------------------------------------------------------------
+-- Operations on the index
+
+-- predⁱ< {i = "i"} _ = "pred i"
+
+predⁱ< : ∀ {n i} → Fin< {suc n} i → Fin n
+predⁱ< {i = suc i} _ = i
+
+-- inject₁ⁱ> {i = "i"} _ = "i"
+
+inject₁ⁱ> : ∀ {n i} → Fin> {suc n} i → Fin n
+inject₁ⁱ>         zero    = zero
+inject₁ⁱ>         (suc _) = zero
+inject₁ⁱ> {suc _} (inj j) = suc (inject₁ⁱ> j)
+
+------------------------------------------------------------------------
+-- Operations
+
+punchIn> : ∀ {n i} → Fin> {suc n} (inject₁ i) → Fin> i → Fin> (inject₁ i)
+punchIn> {i = zero}  zero    k       = suc k
+punchIn> {i = zero}  (suc j) zero    = zero
+punchIn> {i = zero}  (suc j) (suc k) = suc (punchIn> j k)
+punchIn> {i = suc _} (inj j) (inj k) = inj (punchIn> j k)
+
+punchOut> : ∀ {n i j k} → raise!> {n} {i} j ≢ raise!> {n} {i} k → Fin> (inject₁ⁱ> j)
+punchOut>               {j = zero}        {zero}  j≢k = ⊥-elim (j≢k refl)
+punchOut>               {j = zero}        {suc k} j≢k = k
+punchOut> {suc (suc _)} {j = suc j}       {zero}  j≢k = zero
+punchOut> {suc (suc _)} {j = suc zero}    {suc k} j≢k = suc (punchOut> (j≢k ∘ cong suc))
+punchOut> {suc (suc _)} {j = suc (suc j)} {suc k} j≢k = suc (punchOut> {j = suc j} (j≢k ∘ cong suc))
+punchOut> {suc _}       {j = inj j}       {inj k} j≢k = inj (punchOut> (j≢k ∘ cong suc))
 
-inject>′ : ∀ {n i j} → Fin>′ {n} {i} j → Fin> {n} i
-inject>′ zero    = zero
-inject>′ (suc k) = suc (inject>′ k)
-inject>′ (inj k) = inj (inject>′ k)
+-- reflect "j" _ ≡ "j"
 
-cast>-inject<! : ∀ {n i} (j : Fin< (suc i)) → Fin> {suc n} i → Fin> (inject<! j)
-cast>-inject<!         zero    zero    = zero
-cast>-inject<!         zero    (suc k) = suc (cast>-inject<! zero k)
-cast>-inject<! {suc n} zero    (inj k) = suc (cast>-inject<! zero k)
-cast>-inject<! {suc n} (suc j) (inj k) = inj (cast>-inject<! j k)
+reflect! :
+  ∀ {n i} → (j : Fin< (suc {n} i)) → (k : Fin<< (suc j)) → Fin> (inject₁ (inject!< (inject!<< k)))
+reflect! {suc _}               zero    zero    = zero
+reflect! {suc (suc _)} {suc _} (suc j) zero    = suc (reflect! j zero)
+reflect! {suc (suc _)} {suc _} (suc j) (suc k) = inj (reflect! j k)
 
 reflect :
-  ∀ {n i} → (j : Fin< {suc (suc n)} (suc i)) → (k : Fin<′ (suc j)) → Fin> (inject<! (inject<!′ k))
-reflect                 zero    zero    = zero
-reflect {suc n} {suc i} (suc j) zero    = suc (reflect j zero)
-reflect {suc n} {suc i} (suc j) (suc k) = inj (reflect j k)
+  ∀ {n i} → (j : Fin< {n} i) → (k : Fin<< (suc j)) → Fin> (inject< (inject!<< k))
+reflect {suc (suc n)}               zero    zero    = zero
+reflect {_}           {suc (suc _)} (suc j) zero    = suc (reflect j zero)
+reflect {_}           {suc (suc _)} (suc j) (suc k) = inj (reflect j k)
diff --git a/src/Cfe/Fin/Properties.agda b/src/Cfe/Fin/Properties.agda
index 56a2c77..c07aa56 100644
--- a/src/Cfe/Fin/Properties.agda
+++ b/src/Cfe/Fin/Properties.agda
@@ -3,31 +3,231 @@
 module Cfe.Fin.Properties where
 
 open import Cfe.Fin.Base
-open import Data.Fin using (zero; suc; toℕ)
-open import Data.Nat using (suc; pred)
+open import Data.Empty using (⊥-elim)
+open import Data.Fin using (zero; suc; toℕ; punchIn; punchOut; inject₁)
+open import Data.Nat using (suc; pred; _≤_; _<_; _≥_; z≤n; s≤s)
+open import Data.Nat.Properties using (suc-injective; pred-mono; module ≤-Reasoning)
+open import Function using (_∘_)
 open import Relation.Binary.PropositionalEquality
 
-inject<!-cong : ∀ {n i j k l} → toℕ< {i = i} k ≡ toℕ< {i = j} l → inject<! {n} k ≡ inject<! l
-inject<!-cong {suc _} {k = zero}  {zero}  _   = refl
-inject<!-cong {suc _} {k = suc k} {suc l} k≡l = cong suc (inject<!-cong (cong pred k≡l))
-
-raise>-cong : ∀ {n i j k l} → toℕ> {i = i} k ≡ toℕ> {i = j} l → raise> {n} k ≡ raise> l
-raise>-cong {suc _} {k = zero}  {zero}  _   = refl
-raise>-cong {suc _} {k = suc k} {suc l} k≡l = cong suc (raise>-cong (cong pred k≡l))
-raise>-cong {suc _} {k = suc k} {inj l} k≡l = cong suc (raise>-cong (cong pred k≡l))
-raise>-cong {suc _} {k = inj k} {suc l} k≡l = cong suc (raise>-cong (cong pred k≡l))
-raise>-cong {suc _} {k = inj k} {inj l} k≡l = cong suc (raise>-cong (cong pred k≡l))
-
-toℕ>-suc> : ∀ {n} j → toℕ> (suc> {suc n} j) ≡ toℕ> (suc j)
-toℕ>-suc> zero    = refl
-toℕ>-suc> (suc j) = cong suc (toℕ>-suc> j)
-
-toℕ<-inject<! : ∀ {n i} j → toℕ (inject<! {n} {i} j) ≡ toℕ< j
-toℕ<-inject<! {suc n} zero    = refl
-toℕ<-inject<! {suc n} (suc j) = cong suc (toℕ<-inject<! j)
-
-toℕ>-cast>-inject<! : ∀ {n i} j k → toℕ> k ≡ toℕ> (cast>-inject<! {n} {i} j k)
-toℕ>-cast>-inject<!         zero    zero    = refl
-toℕ>-cast>-inject<!         zero    (suc k) = cong suc (toℕ>-cast>-inject<! zero k)
-toℕ>-cast>-inject<! {suc n} zero    (inj k) = cong suc (toℕ>-cast>-inject<! zero k)
-toℕ>-cast>-inject<! {suc n} (suc j) (inj k) = cong suc (toℕ>-cast>-inject<! j k)
+------------------------------------------------------------------------
+-- Properties missing from Data.Fin.Properties
+------------------------------------------------------------------------
+
+inject₁-mono : ∀ {n i j} → toℕ {n} i ≤ toℕ {n} j → toℕ (inject₁ i) ≤ toℕ (inject₁ j)
+inject₁-mono {i = zero}          i≤j       = z≤n
+inject₁-mono {i = suc i} {suc j} (s≤s i≤j) = s≤s (inject₁-mono i≤j)
+
+------------------------------------------------------------------------
+-- Properties of toℕ<
+------------------------------------------------------------------------
+
+toℕ<<i : ∀ {n i} j → toℕ< {n} {i} j < toℕ i
+toℕ<<i zero    = s≤s z≤n
+toℕ<<i (suc j) = s≤s (toℕ<<i j)
+
+------------------------------------------------------------------------
+-- Properties of toℕ>
+
+toℕ>≥i : ∀ {n i} j → toℕ> {n} {i} j ≥ toℕ i
+toℕ>≥i zero    = z≤n
+toℕ>≥i (suc j) = z≤n
+toℕ>≥i (inj j) = s≤s (toℕ>≥i j)
+
+------------------------------------------------------------------------
+-- Properties of inject!<
+------------------------------------------------------------------------
+
+toℕ-inject!< : ∀ {n i} j → toℕ (inject!< {n} {i} j) ≡ toℕ< j
+toℕ-inject!< {suc _} zero    = refl
+toℕ-inject!< {suc _} (suc j) = cong suc (toℕ-inject!< j)
+
+inject!<-mono :
+  ∀ {m n i j k l} → toℕ< k ≤ toℕ< l → toℕ (inject!< {m} {i} k) ≤ toℕ (inject!< {n} {j} l)
+inject!<-mono {k = k} {l} k≤l = begin
+  toℕ (inject!< k) ≡⟨ toℕ-inject!< k ⟩
+  toℕ< k           ≤⟨ k≤l ⟩
+  toℕ< l           ≡˘⟨ toℕ-inject!< l ⟩
+  toℕ (inject!< l) ∎
+  where open ≤-Reasoning
+
+inject!<-cong :
+  ∀ {m n i j k l} → toℕ< k ≡ toℕ< l → toℕ (inject!< {m} {i} k) ≡ toℕ (inject!< {n} {j} l)
+inject!<-cong {k = k} {l} k≡l = begin
+  toℕ (inject!< k) ≡⟨ toℕ-inject!< k ⟩
+  toℕ< k           ≡⟨ k≡l ⟩
+  toℕ< l           ≡˘⟨ toℕ-inject!< l ⟩
+  toℕ (inject!< l) ∎
+  where open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- Properties of inject*<*
+------------------------------------------------------------------------
+
+inject-square : ∀ {n i j} k → inject< (inject!<< {n} {i} {j} k) ≡ inject!< (inject<< k)
+inject-square {suc n} {suc i} zero    = refl
+inject-square {suc n} {suc i} (suc k) = cong suc (inject-square k)
+
+------------------------------------------------------------------------
+-- Properties of strengthen<
+------------------------------------------------------------------------
+
+toℕ-strengthen< : ∀ {n} i → toℕ< (strengthen< {n} i) ≡ toℕ i
+toℕ-strengthen< zero    = refl
+toℕ-strengthen< (suc i) = cong suc (toℕ-strengthen< i)
+
+strengthen<-inject!< : ∀ {n i} j → toℕ< (strengthen< (inject!< {n} {i} j)) ≡ toℕ< j
+strengthen<-inject!< {suc _} zero    = refl
+strengthen<-inject!< {suc _} (suc j) = cong suc (strengthen<-inject!< j)
+
+------------------------------------------------------------------------
+-- Properties of cast<
+------------------------------------------------------------------------
+
+toℕ-cast< : ∀ {m n i j} i≡j k → toℕ< (cast< {m} {n} {i} {j} i≡j k) ≡ toℕ< k
+toℕ-cast< {i = suc _} {suc _} i≡j zero    = refl
+toℕ-cast< {i = suc _} {suc _} i≡j (suc k) = cong suc (toℕ-cast< (cong pred i≡j) k)
+
+------------------------------------------------------------------------
+-- Properties of cast>
+------------------------------------------------------------------------
+
+toℕ-cast> : ∀ {n i j} j≤i k → toℕ> (cast> {n} {i} {j} j≤i k) ≡ toℕ> k
+toℕ-cast> {_}           {zero}  {zero}  j≤i zero    = refl
+toℕ-cast> {_}           {zero}  {zero}  j≤i (suc k) = cong suc (toℕ-cast> j≤i k)
+toℕ-cast> {suc (suc n)} {suc i} {zero}  j≤i (inj k) = cong suc (toℕ-cast> z≤n k)
+toℕ-cast> {suc (suc n)} {suc i} {suc j} j≤i (inj k) = cong suc (toℕ-cast> (pred-mono j≤i) k)
+
+------------------------------------------------------------------------
+-- Properties of raise!>
+------------------------------------------------------------------------
+
+toℕ-raise!> : ∀ {n i} j → toℕ (raise!> {n} {i} j) ≡ toℕ> j
+toℕ-raise!>         zero    = refl
+toℕ-raise!>         (suc j) = cong suc (toℕ-raise!> j)
+toℕ-raise!> {suc n} (inj j) = cong suc (toℕ-raise!> j)
+
+raise!>-cong : ∀ {m n i j k l} → toℕ> k ≡ toℕ> l → toℕ (raise!> {m} {i} k) ≡ toℕ (raise!> {n} {j} l)
+raise!>-cong {k = k} {l} k≡l = begin
+  toℕ (raise!> k) ≡⟨ toℕ-raise!> k ⟩
+  toℕ> k         ≡⟨ k≡l ⟩
+  toℕ> l         ≡˘⟨ toℕ-raise!> l ⟩
+  toℕ (raise!> l) ∎
+  where open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- Properties of suc>
+------------------------------------------------------------------------
+
+toℕ-suc> : ∀ {n i} j → toℕ> (suc> {n} {i} j) ≡ suc (toℕ> j)
+toℕ-suc> zero    = refl
+toℕ-suc> (suc j) = cong suc (toℕ-suc> j)
+toℕ-suc> (inj j) = cong suc (toℕ-suc> j)
+
+------------------------------------------------------------------------
+-- Properties of predⁱ<
+------------------------------------------------------------------------
+
+toℕ-predⁱ< : ∀ {n i} j → suc (toℕ (predⁱ< {n} {i} j)) ≡ toℕ i
+toℕ-predⁱ< {i = suc _} _ = refl
+
+predⁱ<-mono :
+  ∀ {n i j} k l → toℕ i ≤ toℕ j → toℕ (predⁱ< {n} {i} k) ≤ toℕ (predⁱ< {n} {j} l)
+predⁱ<-mono {i = i} {j} k l i≤j = pred-mono (begin
+  suc (toℕ (predⁱ< k)) ≡⟨ toℕ-predⁱ< k ⟩
+  toℕ i                ≤⟨ i≤j ⟩
+  toℕ j                ≡˘⟨ toℕ-predⁱ< l ⟩
+  suc (toℕ (predⁱ< l)) ∎)
+  where open ≤-Reasoning
+
+predⁱ<-cong :
+  ∀ {n i j} k l → toℕ i ≡ toℕ j → toℕ (predⁱ< {n} {i} k) ≡ toℕ (predⁱ< {n} {j} l)
+predⁱ<-cong {i = i} {j} k l i≡j = suc-injective (begin
+  suc (toℕ (predⁱ< k)) ≡⟨ toℕ-predⁱ< k ⟩
+  toℕ i                ≡⟨ i≡j ⟩
+  toℕ j                ≡˘⟨ toℕ-predⁱ< l ⟩
+  suc (toℕ (predⁱ< l)) ∎)
+  where open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- Properties of inject₁ⁱ>
+------------------------------------------------------------------------
+
+toℕ-inject₁ⁱ> : ∀ {n i} j → toℕ (inject₁ⁱ> {n} {i} j) ≡ toℕ i
+toℕ-inject₁ⁱ> {suc _} zero    = refl
+toℕ-inject₁ⁱ> {suc _} (suc k) = refl
+toℕ-inject₁ⁱ> {suc _} (inj k) = cong suc (toℕ-inject₁ⁱ> k)
+
+inject₁ⁱ>-mono :
+  ∀ {n i j} k l → toℕ i ≤ toℕ j → toℕ (inject₁ⁱ> {n} {i} k) ≤ toℕ (inject₁ⁱ> {n} {j} l)
+inject₁ⁱ>-mono {i = i} {j} k l i≤j = begin
+  toℕ (inject₁ⁱ> k) ≡⟨ toℕ-inject₁ⁱ> k ⟩
+  toℕ i             ≤⟨ i≤j ⟩
+  toℕ j             ≡˘⟨ toℕ-inject₁ⁱ> l ⟩
+  toℕ (inject₁ⁱ> l) ∎
+  where open ≤-Reasoning
+
+inject₁ⁱ>-cong :
+  ∀ {n i j} k l → toℕ i ≡ toℕ j → toℕ (inject₁ⁱ> {n} {i} k) ≡ toℕ (inject₁ⁱ> {n} {j} l)
+inject₁ⁱ>-cong {i = i} {j} k l i≡j = begin
+  toℕ (inject₁ⁱ> k) ≡⟨ toℕ-inject₁ⁱ> k ⟩
+  toℕ i             ≡⟨ i≡j ⟩
+  toℕ j             ≡˘⟨ toℕ-inject₁ⁱ> l ⟩
+  toℕ (inject₁ⁱ> l) ∎
+  where open ≡-Reasoning
+
+------------------------------------------------------------------------
+-- Properties of punchIn>
+------------------------------------------------------------------------
+
+toℕ-punchIn> : ∀ {n i} j k → toℕ> (punchIn> {suc n} {i} j k) ≡ toℕ (punchIn (raise!> j) (raise!> k))
+toℕ-punchIn> {_}     {zero}  zero    k       = sym (cong suc (toℕ-raise!> k))
+toℕ-punchIn> {_}     {zero}  (suc j) zero    = refl
+toℕ-punchIn> {_}     {zero}  (suc j) (suc k) = cong suc (toℕ-punchIn> j k)
+toℕ-punchIn> {suc _} {suc i} (inj j) (inj k) = cong suc (toℕ-punchIn> j k)
+
+------------------------------------------------------------------------
+-- Properties of punchOut>
+------------------------------------------------------------------------
+
+toℕ-punchOut> : ∀ {n i j k} j≢k → toℕ> (punchOut> {suc n} {i} {j} {k} j≢k) ≡ toℕ (punchOut j≢k)
+toℕ-punchOut> {_}     {_}           {zero}        {zero}  j≢k = ⊥-elim (j≢k refl)
+toℕ-punchOut> {_}     {_}           {zero}        {suc k} j≢k = sym (toℕ-raise!> k)
+toℕ-punchOut> {suc _} {_}           {suc j}       {zero}  j≢k = refl
+toℕ-punchOut> {suc _} {_}           {suc zero}    {suc k} j≢k =
+  cong suc (toℕ-punchOut> (j≢k ∘ cong suc))
+toℕ-punchOut> {suc _} {_}           {suc (suc j)} {suc k} j≢k =
+  cong suc (toℕ-punchOut> {j = suc j} (j≢k ∘ cong suc))
+toℕ-punchOut> {suc _} {suc zero}    {inj j}       {inj k} j≢k =
+  cong suc (toℕ-punchOut> (j≢k ∘ cong suc))
+toℕ-punchOut> {suc _} {suc (suc _)} {inj j}       {inj k} j≢k =
+  cong suc (toℕ-punchOut> (j≢k ∘ cong suc))
+
+------------------------------------------------------------------------
+-- Properties of reflect!
+------------------------------------------------------------------------
+
+toℕ-reflect! : ∀ {n i} j k → toℕ> (reflect! {n} {i} j k) ≡ toℕ< j
+toℕ-reflect! {suc _}               zero    zero    = refl
+toℕ-reflect! {suc (suc _)} {suc _} (suc j) zero    = cong suc (toℕ-reflect! j zero)
+toℕ-reflect! {suc (suc _)} {suc _} (suc j) (suc k) = cong suc (toℕ-reflect! j k)
+
+------------------------------------------------------------------------
+-- Properties of reflect
+------------------------------------------------------------------------
+
+toℕ-reflect : ∀ {n i} j k → toℕ> (reflect {n} {i} j k) ≡ toℕ< j
+toℕ-reflect {suc (suc _)}               zero    zero    = refl
+toℕ-reflect {_}           {suc (suc _)} (suc j) zero    = cong suc (toℕ-reflect j zero)
+toℕ-reflect {_}           {suc (suc _)} (suc j) (suc k) = cong suc (toℕ-reflect j k)
+
+------------------------------------------------------------------------
+-- Other properties
+------------------------------------------------------------------------
+
+inj-punchOut :
+  ∀ {n i j k} → (j≢k : inject!< {suc n} {suc i} j ≢ raise!> (inj {suc n} {i} k)) →
+  toℕ (punchOut j≢k) ≡ toℕ> k
+inj-punchOut         {j = zero}  {k}     j≢k = toℕ-raise!> k
+inj-punchOut {suc n} {j = suc j} {inj k} j≢k = cong suc (inj-punchOut (j≢k ∘ cong suc))
+