Finally prove that e [ μ e / zero ] ≈ μ e.

Complete proof of generator.

9 files changed, 497 insertions, 186 deletions

diff --git a/src/Cfe/Context/Properties.agda b/src/Cfe/Context/Properties.agda
index 569b72e..933803c 100644
--- a/src/Cfe/Context/Properties.agda
+++ b/src/Cfe/Context/Properties.agda
@@ -20,6 +20,7 @@ open import Cfe.Type over using ()
   ; ≤-trans to ≤ᵗ-trans
   ; ≤-antisym to ≤ᵗ-antisym
   )
+open import Cfe.Vec.Relation.Binary.Pointwise.Inductive
 open import Data.Fin hiding (pred; _≟_) renaming (_≤_ to _≤ᶠ_)
 open import Data.Fin.Properties using (toℕ<n; toℕ-injective; toℕ-inject₁)
   renaming
@@ -47,33 +48,6 @@ private
     n : ℕ
 
 ------------------------------------------------------------------------
--- Properties for Pointwise
-------------------------------------------------------------------------
-
-  pw-antisym :
-    ∀ {a b ℓ} {A : Set a} {B : Set b} {P : REL A B ℓ} {Q : REL B A ℓ} {R : REL A B ℓ} {m n} →
-    Antisym P Q R → Antisym (Pointwise P {m} {n}) (Pointwise Q) (Pointwise R)
-  pw-antisym antisym []       []       = []
-  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 ℓ} {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 _≈_
 ------------------------------------------------------------------------
 -- Relational Properties
@@ -126,7 +100,7 @@ setoid {n} = record { isEquivalence = ≈-isEquivalence {n} }
 ≤-trans = zip (flip ≤ᶠ-trans) (Pw.trans ≤ᵗ-trans)
 
 ≤-antisym : Antisymmetric (_≈_ {n}) _≤_
-≤-antisym = zip (sym ∘₂ ≤ᶠ-antisym) (pw-antisym ≤ᵗ-antisym)
+≤-antisym = zip (sym ∘₂ ≤ᶠ-antisym) (antisym ≤ᵗ-antisym)
 
 ------------------------------------------------------------------------
 -- Structures
@@ -162,7 +136,7 @@ wkn₂-mono :
   τ₁ ≤ᵗ τ₂ → ctx₁ ≤ ctx₂ → wkn₂ {n} ctx₁ i τ₁ ≤ wkn₂ ctx₂ j τ₂
 wkn₂-mono i j {i≡j} τ₁≤τ₂ (g₂≤g₁ , Γ,Δ₁≤Γ,Δ₂) =
   s≤s g₂≤g₁ ,
-  pw-insert
+  Pointwise-insert
     (inject!< i) (inject!< j)
     {i≡j |> toWitness |> inject!<-cong |> fromWitness}
     τ₁≤τ₂
@@ -205,7 +179,7 @@ wkn₁-mono {_} {_ ⊐ g₁} {_ ⊐ g₂} i j {i≡j} τ₁≤τ₂ (g₂≤g₁
     toℕ g₂           ≤⟨ g₂≤g₁ ⟩
     toℕ g₁           ≡˘⟨ toℕ-inject₁ g₁ ⟩
     toℕ (inject₁ g₁) ∎) ,
-  pw-insert
+  Pointwise-insert
     (raise!> i) (raise!> j)
     {i≡j |> toWitness |> raise!>-cong |> fromWitness}
     τ₁≤τ₂
@@ -318,7 +292,11 @@ remove₂-mono :
   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} Γ,Δ₁≤Γ,Δ₂
+  Pointwise-remove
+    (inject!< i)
+    (inject!< j)
+    {i≡j |> toWitness |> inject!<-cong |> fromWitness}
+    Γ,Δ₁≤Γ,Δ₂
 
 remove₂-cong :
   ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ< i ≟ toℕ< j)} →
@@ -356,7 +334,11 @@ remove₁-mono :
   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} Γ,Δ₁≤Γ,Δ₂
+  Pointwise-remove
+    (raise!> i)
+    (raise!> j)
+    {i≡j |> toWitness |> raise!>-cong |> fromWitness}
+    Γ,Δ₁≤Γ,Δ₂
 
 remove₁-cong :
   ∀ {ctx₁ ctx₂} i j {i≡j : True (toℕ> i ≟ toℕ> j)} →
diff --git a/src/Cfe/Derivation/Properties.agda b/src/Cfe/Derivation/Properties.agda
index d922f2a..99be370 100644
--- a/src/Cfe/Derivation/Properties.agda
+++ b/src/Cfe/Derivation/Properties.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary using (Rel; Setoid)
 
 module Cfe.Derivation.Properties
   {c ℓ} (over : Setoid c ℓ)
@@ -8,30 +8,39 @@ module Cfe.Derivation.Properties
 
 open Setoid over using () renaming (Carrier to C)
 
-open import Cfe.Context over using (∙,∙)
+open import Cfe.Context over using (_⊐_; Γ,Δ; ∙,∙; remove₁) renaming (wkn₂ to wkn₂ᶜ)
 open import Cfe.Derivation.Base over
 open import Cfe.Expression over
-open import Cfe.Fin using (zero)
+open import Cfe.Fin using (zero; inj; raise!>; cast>)
 open import Cfe.Judgement over
 open import Cfe.Language over hiding (_∙_)
+  renaming (_≈_ to _≈ˡ_; ≈-refl to ≈ˡ-refl; ≈-reflexive to ≈ˡ-reflexive; ≈-sym to ≈ˡ-sym)
 open import Cfe.Type over using (_⊛_; _⊨_)
-open import Data.Fin using (zero)
-open import Data.List using (List; []; length)
-open import Data.List.Relation.Binary.Pointwise using ([]; _∷_)
-open import Data.Nat.Properties using (n<1+n; module ≤-Reasoning)
-open import Data.Product using (_×_; _,_; -,_)
-open import Data.Sum using (inj₁; inj₂)
-open import Data.Vec using ([]; [_])
-open import Data.Vec.Relation.Binary.Pointwise.Inductive using ([]; _∷_)
-open import Function using (_∘_)
+open import Cfe.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise-insert)
+open import Data.Empty using (⊥-elim)
+open import Data.Fin using (Fin; zero; suc; _≟_; punchOut; punchIn)
+open import Data.Fin.Properties using (punchIn-punchOut)
+open import Data.List using (List; []; length; _++_)
+open import Data.List.Properties using (length-++)
+open import Data.List.Relation.Binary.Equality.Setoid over using (_≋_; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise using (Pointwise-length)
+open import Data.Nat using (ℕ; zero; suc; z≤n; s≤s; _+_) renaming (_≤_ to _≤ⁿ_)
+open import Data.Nat.Properties using (n<1+n; m≤m+n; m≤n+m; m≤n⇒m<n∨m≡n; module ≤-Reasoning)
+open import Data.Product using (_×_; _,_; -,_; ∃-syntax; map₂; proj₁; proj₂)
+open import Data.Sum using (inj₁; inj₂; [_,_]′)
+open import Data.Vec using ([]; _∷_; [_]; lookup; insert)
+open import Data.Vec.Properties using (insert-lookup; insert-punchIn)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pw using ([]; _∷_)
+open import Function using (_∘_; _|>_; _on_; flip)
 open import Induction.WellFounded
-open import Level using (_⊔_)
-open import Relation.Binary.PropositionalEquality using (refl)
-import Relation.Binary.Reasoning.PartialOrder (⊆-poset {c ⊔ ℓ}) as ⊆-Reasoning
-open import Relation.Nullary using (¬_)
+open import Level using (_⊔_; lift)
+open import Relation.Binary.Construct.On using () renaming (wellFounded to on-wellFounded)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
+open import Relation.Nullary
+open import Relation.Nullary.Decidable using (fromWitness)
 
-w∈⟦e⟧⇒e⤇w : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {w} → w ∈ ⟦ e ⟧ [] → e ⤇ w
-w∈⟦e⟧⇒e⤇w {e = e} ctx⊢e∶τ {w} w∈⟦e⟧ = All.wfRec <ₗₑₓ-wellFounded _ Pred go (w , e) ctx⊢e∶τ w∈⟦e⟧
+parse : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {w} → w ∈ ⟦ e ⟧ [] → e ⤇ w
+parse {e = e} ctx⊢e∶τ {w} w∈⟦e⟧ = All.wfRec <ₗₑₓ-wellFounded _ Pred go (w , e) ctx⊢e∶τ w∈⟦e⟧
   where
   Pred : (List C × Expression 0) → Set _
   Pred (w , e) = ∀ {τ} → ∙,∙ ⊢ e ∶ τ → w ∈ ⟦ e ⟧ [] → e ⤇ w
@@ -55,14 +64,14 @@ w∈⟦e⟧⇒e⤇w {e = e} ctx⊢e∶τ {w} w∈⟦e⟧ = All.wfRec <ₗₑₓ-
 
     ⟦μe⟧⊆⟦e[μe/0]⟧ : ⟦ μ e ⟧ [] ⊆ ⟦ e [ μ e / zero ] ⟧ []
     ⟦μe⟧⊆⟦e[μe/0]⟧ = begin
-      ⟦ μ e ⟧ []              ≤⟨ ⋃-unroll (⟦⟧-mono-env e ∘ (_∷ [])) ⟩
-      ⟦ e ⟧ [ ⟦ μ e ⟧ [] ]    ≈˘⟨ subst-cong e (μ e) zero [] ⟩
+      ⟦ μ e ⟧ []              ⊆⟨  ⋃-unroll (⟦⟧-mono-env e ∘ (_∷ [])) ⟩
+      ⟦ e ⟧ [ ⟦ μ e ⟧ [] ]    ≈˘⟨ ⟦⟧-subst e (μ e) zero [] ⟩
       ⟦ e [ μ e / zero ] ⟧ [] ∎
       where open ⊆-Reasoning
   go (w  , e₁ ∙ e₂) rec (Cat ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁⊛τ₂) (w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq) =
     Cat
-      (rec (w₁ , e₁) (lex-∙ˡ e₁ e₂ []        (-, -, w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq)) ctx⊢e₁∶τ₁ w₁∈⟦e₁⟧)
-      (rec (w₂ , e₂) (lex-∙ʳ e₁ e₂ [] ε∉⟦e₁⟧ (-, -, w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq)) ctx⊢e₂∶τ₂ w₂∈⟦e₂⟧)
+      (rec (w₁ , e₁) (lex-∙ˡ e₁ e₂ w₁ eq) ctx⊢e₁∶τ₁ w₁∈⟦e₁⟧)
+      (rec (w₂ , e₂) (lex-∙ʳ e₁ e₂ [] ε∉⟦e₁⟧ w₁∈⟦e₁⟧ eq) ctx⊢e₂∶τ₂ w₂∈⟦e₂⟧)
       eq
     where
     open _⊛_ τ₁⊛τ₂ using (¬n₁)
@@ -72,3 +81,37 @@ w∈⟦e⟧⇒e⤇w {e = e} ctx⊢e∶τ {w} w∈⟦e⟧ = All.wfRec <ₗₑₓ-
     Veeˡ (rec (w , e₁) (inj₂ (refl , rank-∨ˡ e₁ e₂)) ctx⊢e₁∶τ₁ w∈⟦e₁⟧)
   go (w , e₁ ∨ e₂) rec (Vee ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁#τ₂) (inj₂ w∈⟦e₂⟧) =
     Veeʳ (rec (w , e₂) (inj₂ (refl , rank-∨ʳ e₁ e₂)) ctx⊢e₂∶τ₂ w∈⟦e₂⟧)
+
+generate : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {w} → e ⤇ w → w ∈ ⟦ e ⟧ []
+generate {e = e} ctx⊢e∶τ {w} e⤇w = All.wfRec <ₗₑₓ-wellFounded _ Pred go (w , e) ctx⊢e∶τ e⤇w
+  where
+  Pred : (List C × Expression 0) → Set _
+  Pred (w , e) = ∀ {τ} → ∙,∙ ⊢ e ∶ τ → e ⤇ w → w ∈ ⟦ e ⟧ []
+
+  go : ∀ w,e → WfRec _<ₗₑₓ_ Pred w,e → Pred w,e
+  go (w , ε)       rec Eps      Eps = lift refl
+  go (w , Char c)  rec (Char c) (Char c∼y) = c∼y ∷ []
+  go (w , μ e)     rec (Fix ctx⊢e∶τ) (Fix e[μe/0]⤇w) = ∈-resp-≈ (μ-roll e []) w∈⟦e[μe/0]⟧
+    where
+    w,e[μe/0]<ₗₑₓw,μe : (w , e [ μ e / zero ]) <ₗₑₓ (w , μ e)
+    w,e[μe/0]<ₗₑₓw,μe = inj₂ (refl , (begin-strict
+      rank (e [ μ e / zero ]) ≡⟨ subst₂-pres-rank ctx⊢e∶τ zero (Fix ctx⊢e∶τ) ⟩
+      rank e                  <⟨ rank-μ e ⟩
+      rank (μ e)              ∎))
+      where open ≤-Reasoning
+
+    w∈⟦e[μe/0]⟧ : w ∈ ⟦ e [ μ e / zero ] ⟧ []
+    w∈⟦e[μe/0]⟧ = rec (w , e [ μ e / zero ]) w,e[μe/0]<ₗₑₓw,μe (subst₂ ctx⊢e∶τ zero (Fix ctx⊢e∶τ)) e[μe/0]⤇w
+  go (w , e₁ ∙ e₂) rec (Cat ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁⊛τ₂) (Cat {w₁ = w₁} {w₂} e₁⤇w₁ e₂⤇w₂ eq) =
+    w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq
+    where
+    open _⊛_ τ₁⊛τ₂ using (¬n₁)
+    ε∉⟦e₁⟧ : ¬ Null (⟦ e₁ ⟧ [])
+    ε∉⟦e₁⟧ = ¬n₁ ∘ _⊨_.n⇒n (soundness ctx⊢e₁∶τ₁ [] [])
+
+    w₁∈⟦e₁⟧ = rec (w₁ , e₁) (lex-∙ˡ e₁ e₂ w₁ eq) ctx⊢e₁∶τ₁ e₁⤇w₁
+    w₂∈⟦e₂⟧ = rec (w₂ , e₂) (lex-∙ʳ e₁ e₂ [] ε∉⟦e₁⟧ w₁∈⟦e₁⟧ eq) ctx⊢e₂∶τ₂ e₂⤇w₂
+  go (w , e₁ ∨ e₂) rec (Vee ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁#τ₂) (Veeˡ e₁⤇w) =
+    inj₁ (rec (w , e₁) (inj₂ (refl , rank-∨ˡ e₁ e₂)) ctx⊢e₁∶τ₁ e₁⤇w)
+  go (w , e₁ ∨ e₂) rec (Vee ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁#τ₂) (Veeʳ e₂⤇w) =
+    inj₂ (rec (w , e₂) (inj₂ (refl , rank-∨ʳ e₁ e₂)) ctx⊢e₂∶τ₂ e₂⤇w)
diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index f37694b..933b3bb 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -46,7 +46,7 @@ infix 4 _≈_
 ⟦ Char x ⟧  _ = ｛ x ｝
 ⟦ e₁ ∨ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∪ ⟦ e₂ ⟧ γ
 ⟦ e₁ ∙ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∙ˡ ⟦ e₂ ⟧ γ
-⟦ Var n ⟧   γ = lookup γ n
+⟦ Var j ⟧   γ = lookup γ j
 ⟦ μ e ⟧     γ = ⋃ (λ X → ⟦ e ⟧ (X ∷ γ))
 
 _≈_ : {n : ℕ} → Expression n → Expression n → Set _
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
index d994fe6..e520f7b 100644
--- a/src/Cfe/Expression/Properties.agda
+++ b/src/Cfe/Expression/Properties.agda
@@ -10,7 +10,6 @@ open Setoid over using () renaming (Carrier to C; _≈_ to _∼_)
 
 open import Algebra
 open import Cfe.Expression.Base over
-open import Cfe.Function.Power
 open import Cfe.Language over
   hiding
     ( ≈-isPartialEquivalence; partialSetoid
@@ -33,26 +32,31 @@ open import Cfe.Language over
   ; ∙-zeroʳ to ∙ˡ-zeroʳ
   ; ∙-zero to ∙ˡ-zero
   )
+open import Cfe.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise-insert)
 open import Data.Empty using (⊥-elim)
 open import Data.Fin hiding (_+_; _≤_; _<_)
+open import Data.Fin.Properties using (punchIn-punchOut)
 open import Data.List using (List; length; _++_)
 open import Data.List.Properties using (length-++)
+open import Data.List.Relation.Binary.Equality.Setoid over using (_≋_)
 open import Data.List.Relation.Binary.Pointwise using (Pointwise-length)
 open import Data.Nat hiding (_≟_; _⊔_; _^_)
 open import Data.Nat.Induction using (<-wellFounded)
 open import Data.Nat.Properties hiding (_≟_)
 open import Data.Product
 open import Data.Product.Relation.Binary.Lex.Strict using (×-wellFounded)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import Data.Vec hiding (length; _++_)
+open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
+open import Data.Vec hiding (length; map; _++_)
 open import Data.Vec.Properties
-open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
-  hiding (refl; sym; trans; setoid; lookup)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pw
+  hiding (refl; sym; trans; setoid; lookup; map)
+open import Function using (_∘_; _|>_; id)
 open import Induction.WellFounded using (WellFounded)
 open import Level using (_⊔_)
 open import Relation.Binary.Construct.On using () renaming (wellFounded to on-wellFounded)
 open import Relation.Binary.PropositionalEquality hiding (setoid)
 open import Relation.Nullary
+open import Relation.Nullary.Decidable using (fromWitness)
 
 private
   variable
@@ -71,7 +75,7 @@ private
 ⟦⟧-mono-env (Char _)  mono = ⊆-refl
 ⟦⟧-mono-env (e₁ ∨ e₂) mono = ∪-mono (⟦⟧-mono-env e₁ mono) (⟦⟧-mono-env e₂ mono)
 ⟦⟧-mono-env (e₁ ∙ e₂) mono = ∙-mono (⟦⟧-mono-env e₁ mono) (⟦⟧-mono-env e₂ mono)
-⟦⟧-mono-env (Var j)   mono = PW.lookup mono j
+⟦⟧-mono-env (Var j)   mono = Pw.lookup mono j
 ⟦⟧-mono-env (μ e)     mono = ⋃-mono λ A⊆B → ⟦⟧-mono-env e (A⊆B ∷ mono)
 
 ⟦⟧-cong-env : ∀ (e : Expression n) {γ γ′} → Pointwise _≈ˡ_ γ γ′ → ⟦ e ⟧ γ ≈ˡ ⟦ e ⟧ γ′
@@ -80,7 +84,7 @@ private
 ⟦⟧-cong-env (Char _)  cong = ≈ˡ-refl
 ⟦⟧-cong-env (e₁ ∨ e₂) cong = ∪-cong (⟦⟧-cong-env e₁ cong) (⟦⟧-cong-env e₂ cong)
 ⟦⟧-cong-env (e₁ ∙ e₂) cong = ∙ˡ-cong (⟦⟧-cong-env e₁ cong) (⟦⟧-cong-env e₂ cong)
-⟦⟧-cong-env (Var j)   cong = PW.lookup cong j
+⟦⟧-cong-env (Var j)   cong = Pw.lookup cong j
 ⟦⟧-cong-env (μ e)     cong = ⋃-cong λ A≈B → ⟦⟧-cong-env e (A≈B ∷ cong)
 
 ------------------------------------------------------------------------
@@ -128,10 +132,14 @@ setoid {n} = record { isEquivalence = ≈-isEquivalence {n} }
 -- Definitions
 
 infix 4 _<ₗₑₓ_
+infix 4 _<ₕₑₜ_
 
 _<ₗₑₓ_ : REL (List C × Expression m) (List C × Expression n) _
 (w , e) <ₗₑₓ (w′ , e′) = length w < length w′ ⊎ length w ≡ length w′ × e <ᵣₐₙₖ e′
 
+_<ₕₑₜ_ : Rel (List C × ∃[ m ] Expression m) _
+(w , _ , e) <ₕₑₜ (w′ , _ , e′) = (w , e) <ₗₑₓ (w′ , e′)
+
 ------------------------------------------------------------------------
 -- Relational properties
 
@@ -166,6 +174,9 @@ _<ₗₑₓ_ : REL (List C × Expression m) (List C × Expression n) _
 <ₗₑₓ-wellFounded : WellFounded (_<ₗₑₓ_ {n})
 <ₗₑₓ-wellFounded = on-wellFounded (map₁ length) (×-wellFounded <-wellFounded <ᵣₐₙₖ-wellFounded)
 
+<ₕₑₜ-wellFounded : WellFounded _<ₕₑₜ_
+<ₕₑₜ-wellFounded =
+  on-wellFounded (map length (rank ∘ proj₂)) (×-wellFounded <-wellFounded <-wellFounded)
 
 ------------------------------------------------------------------------
 -- Other properties
@@ -175,26 +186,20 @@ rank-∨ˡ e₁ e₂ = begin-strict
   rank e₁           ≤⟨ m≤m+n (rank e₁) (rank e₂) ⟩
   rank e₁ + rank e₂ <⟨ n<1+n (rank e₁ + rank e₂) ⟩
   rank (e₁ ∨ e₂)    ∎
-  where
-  open ≤-Reasoning
+  where open ≤-Reasoning
 
 rank-∨ʳ : ∀ (e₁ e₂ : Expression n) → e₂ <ᵣₐₙₖ e₁ ∨ e₂
 rank-∨ʳ e₁ e₂ = begin-strict
   rank e₂           ≤⟨ m≤n+m (rank e₂) (rank e₁) ⟩
   rank e₁ + rank e₂ <⟨ n<1+n (rank e₁ + rank e₂) ⟩
   rank (e₁ ∨ e₂)    ∎
-  where
-  open ≤-Reasoning
+  where open ≤-Reasoning
 
 rank-∙ˡ : ∀ (e₁ e₂ : Expression n) → e₁ <ᵣₐₙₖ e₁ ∙ e₂
 rank-∙ˡ e₁ _ = n<1+n (rank e₁)
 
-lex-∙ˡ :
-  ∀ (e₁ e₂ : Expression n) γ →
-  ∀ {w} → (w∈⟦e₁∙e₂⟧ : w ∈ ⟦ e₁ ∙ e₂ ⟧ γ) →
-  let w₁ = proj₁ w∈⟦e₁∙e₂⟧ in
-  (w₁ , e₁) <ₗₑₓ (w , e₁ ∙ e₂)
-lex-∙ˡ e₁ e₂ γ {w} (w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq) with m≤n⇒m<n∨m≡n ∣w₁∣≤∣w∣
+lex-∙ˡ : ∀ (e₁ e₂ : Expression n) → ∀ w₁ {w₂ w} → w₁ ++ w₂ ≋ w → (w₁ , e₁) <ₗₑₓ (w , e₁ ∙ e₂)
+lex-∙ˡ e₁ e₂ w₁ {w₂} {w} eq with m≤n⇒m<n∨m≡n ∣w₁∣≤∣w∣
   where
   open ≤-Reasoning
   ∣w₁∣≤∣w∣ : length w₁ ≤ length w
@@ -208,10 +213,9 @@ lex-∙ˡ e₁ e₂ γ {w} (w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧
 
 lex-∙ʳ :
   ∀ (e₁ e₂ : Expression n) γ → ¬ Null (⟦ e₁ ⟧ γ) →
-  ∀ {w} → (w∈⟦e₁∙e₂⟧ : w ∈ ⟦ e₁ ∙ e₂ ⟧ γ) →
-  let w₂ = proj₁ (proj₂ w∈⟦e₁∙e₂⟧) in
+  ∀ {w₁ w₂ w} → w₁ ∈ ⟦ e₁ ⟧ γ → w₁ ++ w₂ ≋ w →
   (w₂ , e₂) <ₗₑₓ (w , e₁ ∙ e₂)
-lex-∙ʳ e₁ _ γ ε∉⟦e₁⟧ {w} (w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq) with m≤n⇒m<n∨m≡n ∣w₂∣≤∣w∣
+lex-∙ʳ e₁ _ γ ε∉⟦e₁⟧ {w₁} {w₂} {w} w₁∈⟦e₁⟧ eq with m≤n⇒m<n∨m≡n ∣w₂∣≤∣w∣
   where
   open ≤-Reasoning
   ∣w₂∣≤∣w∣ : length w₂ ≤ length w
@@ -223,14 +227,13 @@ lex-∙ʳ e₁ _ γ ε∉⟦e₁⟧ {w} (w₁ , w₂ , w₁∈⟦e₁⟧ , w₂�
 ... | inj₁ ∣w₂∣<∣w∣ = inj₁ ∣w₂∣<∣w∣
 ... | inj₂ ∣w₂∣≡∣w∣ = ⊥-elim (ε∉⟦e₁⟧ (∣w∣≡0+w∈A⇒ε∈A {A = ⟦ e₁ ⟧ γ} ∣w₁∣≡0 w₁∈⟦e₁⟧))
   where
+    open ≤-Reasoning
     ∣w₁∣≡0 : length w₁ ≡ 0
     ∣w₁∣≡0 = +-cancelʳ-≡ (length w₁) 0 (begin-equality
       length w₁ + length w₂ ≡˘⟨ length-++ w₁ ⟩
       length (w₁ ++ w₂)     ≡⟨ Pointwise-length eq ⟩
       length w              ≡˘⟨ ∣w₂∣≡∣w∣ ⟩
       length w₂             ∎)
-      where
-      open ≤-Reasoning
 
 rank-μ : ∀ (e : Expression (suc n)) → e <ᵣₐₙₖ μ e
 rank-μ e = n<1+n (rank e)
@@ -258,15 +261,16 @@ Var-inj : ∀ {j k} → Var {n} j ≈ Var k → j ≡ k
 Var-inj {.(suc _)} {zero}  {zero}  j≈k = refl
 Var-inj {.(suc _)} {zero}  {suc k} j≈k = ⊥-elim (ε∉∅ (Null-resp-≈ ｛ε｝≈∅ ε∈｛ε｝))
   where
-  open import Relation.Binary.Reasoning.Setoid setoidˡ
-  ｛ε｝≈∅ = begin
-    ｛ε｝ {ℓ}              ≈⟨ j≈k (｛ε｝ ∷ replicate ∅) ⟩
+  open ⊆-Reasoning
+  ｛ε｝≈∅ : ｛ε｝ {ℓ} ≈ˡ ∅ {c ⊔ ℓ}
+  ｛ε｝≈∅ = begin-equality
+    ｛ε｝                  ≈⟨ j≈k (｛ε｝ ∷ replicate ∅) ⟩
     lookup (replicate ∅) k ≡⟨ lookup-replicate k ∅ ⟩
     ∅                      ∎
 Var-inj {.(suc _)} {suc j} {zero}  j≈k = ⊥-elim (ε∉∅ (Null-resp-≈ ｛ε｝≈∅ ε∈｛ε｝))
   where
-  open import Relation.Binary.Reasoning.Setoid setoidˡ
-  ｛ε｝≈∅ = begin
+  open ⊆-Reasoning
+  ｛ε｝≈∅ = begin-equality
     ｛ε｝ {ℓ}                  ≡˘⟨ lookup-replicate j ｛ε｝ ⟩
     lookup (replicate ｛ε｝) j ≈⟨ j≈k (∅ ∷ replicate ｛ε｝) ⟩
     ∅                          ∎
@@ -500,31 +504,40 @@ Var-inj {.(suc _)} {suc j} {suc k} j≈k = cong suc (Var-inj λ γ → j≈k (�
 -- Functional properties
 
 μ-cong : μ_ Preserves _≈_ ⟶ (_≈_ {n})
-μ-cong {x = e} {e′} e≈e′ γ = ⋃-cong λ {A} {B} A≈B → begin
-  ⟦ e ⟧ (A ∷ γ) ≈⟨ ⟦⟧-cong-env e (A≈B ∷ PW.refl ≈ˡ-refl) ⟩
+μ-cong {x = e} {e′} e≈e′ γ = ⋃-cong λ {A} {B} A≈B → begin-equality
+  ⟦ e ⟧ (A ∷ γ) ≈⟨ ⟦⟧-cong-env e (A≈B ∷ Pw.refl ≈ˡ-refl) ⟩
   ⟦ e ⟧ (B ∷ γ) ≈⟨ e≈e′ (B ∷ γ) ⟩
   ⟦ e′ ⟧ (B ∷ γ) ∎
-  where
-  open import Relation.Binary.Reasoning.Setoid setoidˡ
+  where open ⊆-Reasoning
 
 ------------------------------------------------------------------------
 -- Properties of wkn
 ------------------------------------------------------------------------
 -- Algebraic properties
 
-wkn-cong : ∀ (e : Expression n) i γ A → ⟦ wkn e i ⟧ (insert γ i A) ≈ˡ ⟦ e ⟧ γ
-wkn-cong ⊥         i γ A = ≈ˡ-refl
-wkn-cong ε         i γ A = ≈ˡ-refl
-wkn-cong (Char _)  i γ A = ≈ˡ-refl
-wkn-cong (e₁ ∨ e₂) i γ A = ∪-cong (wkn-cong e₁ i γ A) (wkn-cong e₂ i γ A)
-wkn-cong (e₁ ∙ e₂) i γ A = ∙ˡ-cong (wkn-cong e₁ i γ A) (wkn-cong e₂ i γ A)
-wkn-cong (Var j)   i γ A = ≈ˡ-reflexive (insert-punchIn γ i A j)
-wkn-cong (μ e)     i γ A = ⋃-cong λ {B} {C} B≈C → begin
-  ⟦ wkn e (suc i) ⟧ (B ∷ insert γ i A) ≈⟨ ⟦⟧-cong-env (wkn e (suc i)) (B≈C ∷ PW.refl ≈ˡ-refl) ⟩
-  ⟦ wkn e (suc i) ⟧ (C ∷ insert γ i A) ≈⟨ wkn-cong e (suc i) (C ∷ γ) A ⟩
+⟦⟧-wkn : ∀ (e : Expression n) i γ A → ⟦ wkn e i ⟧ (insert γ i A) ≈ˡ ⟦ e ⟧ γ
+⟦⟧-wkn ⊥         i γ A = ≈ˡ-refl
+⟦⟧-wkn ε         i γ A = ≈ˡ-refl
+⟦⟧-wkn (Char _)  i γ A = ≈ˡ-refl
+⟦⟧-wkn (e₁ ∨ e₂) i γ A = ∪-cong (⟦⟧-wkn e₁ i γ A) (⟦⟧-wkn e₂ i γ A)
+⟦⟧-wkn (e₁ ∙ e₂) i γ A = ∙ˡ-cong (⟦⟧-wkn e₁ i γ A) (⟦⟧-wkn e₂ i γ A)
+⟦⟧-wkn (Var j)   i γ A = ≈ˡ-reflexive (insert-punchIn γ i A j)
+⟦⟧-wkn (μ e)     i γ A = ⋃-cong λ {B} {C} B≈C → begin-equality
+  ⟦ wkn e (suc i) ⟧ (B ∷ insert γ i A) ≈⟨ ⟦⟧-cong-env (wkn e (suc i)) (B≈C ∷ Pw.refl ≈ˡ-refl) ⟩
+  ⟦ wkn e (suc i) ⟧ (C ∷ insert γ i A) ≈⟨ ⟦⟧-wkn e (suc i) (C ∷ γ) A ⟩
   ⟦ e ⟧ (C ∷ γ)                        ∎
-  where
-  open import Relation.Binary.Reasoning.Setoid setoidˡ
+  where open ⊆-Reasoning
+
+wkn-mono :
+  ∀ (e₁ e₂ : Expression n) i → (∀ γ → ⟦ e₁ ⟧ γ ⊆ ⟦ e₂ ⟧ γ) → ∀ γ → ⟦ wkn e₁ i ⟧ γ ⊆ ⟦ wkn e₂ i ⟧ γ
+wkn-mono e₁ e₂ i mono γ = begin
+  ⟦ wkn e₁ i ⟧ γ                                    ≡˘⟨ cong ⟦ wkn e₁ i ⟧ (insert-remove γ i) ⟩
+  ⟦ wkn e₁ i ⟧ (insert (remove γ i) i (lookup γ i)) ≈⟨  ⟦⟧-wkn e₁ i (remove γ i) (lookup γ i) ⟩
+  ⟦ e₁ ⟧ (remove γ i)                               ⊆⟨  mono (remove γ i) ⟩
+  ⟦ e₂ ⟧ (remove γ i)                               ≈˘⟨ ⟦⟧-wkn e₂ i (remove γ i) (lookup γ i) ⟩
+  ⟦ wkn e₂ i ⟧ (insert (remove γ i) i (lookup γ i)) ≡⟨  cong ⟦ wkn e₂ i ⟧ (insert-remove γ i) ⟩
+  ⟦ wkn e₂ i ⟧ γ                                    ∎
+  where open ⊆-Reasoning
 
 -- Syntactic properties
 
@@ -544,7 +557,7 @@ rank-wkn (μ e)     i = cong suc (rank-wkn e (suc i))
 μ-wkn e γ = ≈ˡ-trans
   (∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G λ
     { 0       → ≈ˡ-refl
-    ; (suc n) → wkn-cong e zero γ (((λ X → ⟦ wkn e zero ⟧ (X ∷ γ)) ^ n) ∅)
+    ; (suc n) → ⟦⟧-wkn e zero γ (Iter (λ X → ⟦ wkn e zero ⟧ (X ∷ γ)) ∅ n)
     })
   (⋃-inverseʳ (⟦ e ⟧ γ))
 
@@ -553,33 +566,167 @@ rank-wkn (μ e)     i = cong suc (rank-wkn e (suc i))
 ------------------------------------------------------------------------
 -- Algebraic properties
 
-subst-cong : ∀ (e : Expression (suc n)) e′ i γ → ⟦ e [ e′ / i ] ⟧ γ ≈ˡ ⟦ e ⟧ (insert γ i (⟦ e′ ⟧ γ))
-subst-cong ⊥         e′ i γ = ≈ˡ-refl
-subst-cong ε         e′ i γ = ≈ˡ-refl
-subst-cong (Char c)  e′ i γ = ≈ˡ-refl
-subst-cong (e₁ ∨ e₂) e′ i γ = ∪-cong (subst-cong e₁ e′ i γ) (subst-cong e₂ e′ i γ)
-subst-cong (e₁ ∙ e₂) e′ i γ = ∙ˡ-cong (subst-cong e₁ e′ i γ) (subst-cong e₂ e′ i γ)
-subst-cong (Var j)   e′ i γ with i ≟ j
+subst-monoʳ :
+  ∀ (e : Expression (suc n)) i {e₁ e₂} → (∀ γ → ⟦ e₁ ⟧ γ ⊆ ⟦ e₂ ⟧ γ) →
+  ∀ γ → ⟦ e [ e₁ / i ] ⟧ γ ⊆ ⟦ e [ e₂ / i ] ⟧ γ
+subst-monoʳ ⊥         i           mono γ = ⊆-refl
+subst-monoʳ ε         i           mono γ = ⊆-refl
+subst-monoʳ (Char c)  i           mono γ = ⊆-refl
+subst-monoʳ (e₁ ∨ e₂) i           mono γ = ∪-mono (subst-monoʳ e₁ i mono γ) (subst-monoʳ e₂ i mono γ)
+subst-monoʳ (e₁ ∙ e₂) i           mono γ = ∙-mono (subst-monoʳ e₁ i mono γ) (subst-monoʳ e₂ i mono γ)
+subst-monoʳ (Var j)   i           mono γ with i ≟ j
+...                                           | yes refl = mono γ
+...                                           | no _     = ⊆-refl
+subst-monoʳ (μ e)     i {e₁} {e₂} mono γ = ⋃-mono (λ {A} {B} A⊆B → begin
+  ⟦ e [ wkn e₁ zero / suc i ] ⟧ (A ∷ γ) ⊆⟨ ⟦⟧-mono-env (e [ wkn e₁ zero / suc i ]) (A⊆B ∷ Pw.refl ⊆-refl) ⟩
+  ⟦ e [ wkn e₁ zero / suc i ] ⟧ (B ∷ γ) ⊆⟨ subst-monoʳ e (suc i) (wkn-mono e₁ e₂ zero mono) (B ∷ γ) ⟩
+  ⟦ e [ wkn e₂ zero / suc i ] ⟧ (B ∷ γ) ∎)
+  where open ⊆-Reasoning
+
+subst-congⁱ : ∀ (e : Expression (suc n)) e′ {i j} → i ≡ j → e [ e′ / i ] ≈ e [ e′ / j ]
+subst-congⁱ e e′ {i} refl = ≈-refl {x = e [ e′ / i ]}
+
+⟦⟧-subst : ∀ (e : Expression (suc n)) e′ i γ → ⟦ e [ e′ / i ] ⟧ γ ≈ˡ ⟦ e ⟧ (insert γ i (⟦ e′ ⟧ γ))
+⟦⟧-subst ⊥         e′ i γ = ≈ˡ-refl
+⟦⟧-subst ε         e′ i γ = ≈ˡ-refl
+⟦⟧-subst (Char c)  e′ i γ = ≈ˡ-refl
+⟦⟧-subst (e₁ ∨ e₂) e′ i γ = ∪-cong (⟦⟧-subst e₁ e′ i γ) (⟦⟧-subst e₂ e′ i γ)
+⟦⟧-subst (e₁ ∙ e₂) e′ i γ = ∙ˡ-cong (⟦⟧-subst e₁ e′ i γ) (⟦⟧-subst e₂ e′ i γ)
+⟦⟧-subst (Var j)   e′ i γ with i ≟ j
 ...                            | yes refl = ≈ˡ-reflexive (sym (insert-lookup γ i (⟦ e′ ⟧ γ)))
-...                            | no i≢j   = ≈ˡ-reflexive (begin
+...                            | no i≢j   = begin-equality
   lookup γ po             ≡˘⟨ cong (λ x → lookup x po) (remove-insert γ i (⟦ e′ ⟧ γ)) ⟩
   lookup (remove γ′ i) po ≡⟨ remove-punchOut γ′ i≢j ⟩
-  lookup γ′ j             ∎)
+  lookup γ′ j             ∎
   where
-  open ≡-Reasoning
+  open ⊆-Reasoning
   po = punchOut i≢j
   γ′ = insert γ i (⟦ e′ ⟧ γ)
-subst-cong (μ e)     e′ i γ = ⋃-cong λ {A} {B} A≈B → begin
-  ⟦ e [ e′′ / suc i ] ⟧ (A ∷ γ)            ≈⟨ ⟦⟧-cong-env (e [ e′′ / suc i ]) (A≈B ∷ PW.refl ≈ˡ-refl) ⟩
-  ⟦ e [ e′′ / suc i ] ⟧ (B ∷ γ)            ≈⟨ subst-cong e e′′ (suc i) (B ∷ γ) ⟩
-  ⟦ e ⟧ (B ∷ insert γ i (⟦ e′′ ⟧ (B ∷ γ))) ≈⟨ ⟦⟧-cong-env e (insert′ (wkn-cong e′ zero γ B) (B ∷ γ) (suc i)) ⟩
+⟦⟧-subst (μ e)     e′ i γ = ⋃-cong λ {A} {B} A≈B → begin-equality
+  ⟦ e [ e′′ / suc i ] ⟧ (A ∷ γ)            ≈⟨ ⟦⟧-cong-env (e [ e′′ / suc i ]) (A≈B ∷ Pw.refl ≈ˡ-refl) ⟩
+  ⟦ e [ e′′ / suc i ] ⟧ (B ∷ γ)            ≈⟨ ⟦⟧-subst e e′′ (suc i) (B ∷ γ) ⟩
+  ⟦ e ⟧ (B ∷ insert γ i (⟦ e′′ ⟧ (B ∷ γ))) ≈⟨ ⟦⟧-cong-env e (insert′ (⟦⟧-wkn e′ zero γ B) (B ∷ γ) (suc i)) ⟩
   ⟦ e ⟧ (B ∷ insert γ i (⟦ e′ ⟧ γ))        ∎
   where
-  open import Relation.Binary.Reasoning.Setoid setoidˡ
+  open ⊆-Reasoning
   e′′ = wkn e′ zero
 
   insert′ :
     ∀ {n} {x y : Language (c ⊔ ℓ)} (x≈y : x ≈ˡ y) xs i →
     Pointwise _≈ˡ_ {n = suc n} (insert xs i x) (insert xs i y)
-  insert′ x≈y xs        zero   = x≈y ∷ PW.refl ≈ˡ-refl
+  insert′ x≈y xs        zero   = x≈y ∷ Pw.refl ≈ˡ-refl
   insert′ x≈y (x ∷ xs) (suc i) = ≈ˡ-refl ∷ insert′ x≈y xs i
+
+------------------------------------------------------------------------
+-- Other properties
+
+μ-roll : ∀ (e : Expression (suc n)) → e [ μ e / zero ] ≈ μ e
+μ-roll e γ =
+  ⊆-antisym
+    (begin
+      ⟦ e [ μ e / zero ] ⟧ γ ≈⟨ ⟦⟧-subst e (μ e) zero γ ⟩
+      ⟦ e ⟧ (⟦ μ e ⟧ γ ∷ γ)  ⊆⟨ big-bit ⟩
+      ⟦ μ e ⟧ γ              ∎)
+    (begin
+      ⟦ μ e ⟧ γ              ⊆⟨  ⋃-unroll (⟦⟧-mono-env e ∘ (_∷ Pw.refl ⊆-refl)) ⟩
+      ⟦ e ⟧ (⟦ μ e ⟧ γ ∷ γ)  ≈˘⟨ ⟦⟧-subst e (μ e) zero γ ⟩
+      ⟦ e [ μ e / zero ] ⟧ γ ∎)
+  where
+  open ⊆-Reasoning
+
+  get-tag :
+    ∀ {m} e A (K : ℕ → Language _) →
+    (∀ {w} → w ∈ A → ∃[ n ] w ∈ K n) → (∀ {m n} → m ≤ n → K m ⊆ K n) →
+    ∀ i γ {w} → w ∈ ⟦ e ⟧ (insert {n = m} γ i A) → ∃[ n ] w ∈ ⟦ e ⟧ (insert γ i (K n))
+  get-tag ε         A K tag mono i γ w∈⟦e⟧ = 0 , w∈⟦e⟧
+  get-tag (Char c)  A K tag mono i γ w∈⟦e⟧ = 0 , w∈⟦e⟧
+  get-tag (e₁ ∨ e₂) A K tag mono i γ w∈⟦e⟧ =
+    [ map₂ inj₁ ∘ get-tag e₁ A K tag mono i γ
+    , map₂ inj₂ ∘ get-tag e₂ A K tag mono i γ
+    ]′ w∈⟦e⟧
+  get-tag (e₁ ∙ e₂) A K tag mono i γ (w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq) =
+    ( n₁ + n₂
+    , w₁
+    , w₂
+    , ∈-resp-⊆
+      (⟦⟧-mono-env
+        e₁
+        (Pointwise-insert i i {fromWitness refl} (mono (m≤m+n n₁ n₂)) (Pw.refl ⊆-refl)))
+      w₁∈⟦e₁⟧′
+    , ∈-resp-⊆
+      (⟦⟧-mono-env
+        e₂
+        (Pointwise-insert i i {fromWitness refl} (mono (m≤n+m n₂ n₁)) (Pw.refl ⊆-refl)))
+      w₂∈⟦e₂⟧′
+    , eq
+    )
+    where
+    n₁,w₁∈⟦e₁⟧′ = get-tag e₁ A K tag mono i γ w₁∈⟦e₁⟧
+    n₂,w₂∈⟦e₂⟧′ = get-tag e₂ A K tag mono i γ w₂∈⟦e₂⟧
+
+    n₁       = proj₁ n₁,w₁∈⟦e₁⟧′
+    n₂       = proj₁ n₂,w₂∈⟦e₂⟧′
+    w₁∈⟦e₁⟧′ = proj₂ n₁,w₁∈⟦e₁⟧′
+    w₂∈⟦e₂⟧′ = proj₂ n₂,w₂∈⟦e₂⟧′
+  get-tag (Var j)   A K tag mono i γ {w} w∈⟦e⟧ with i ≟ j
+  ... | yes refl =
+    map₂
+      (λ {n} → K n |> insert-lookup γ j |> ≈ˡ-reflexive |> ≈ˡ-sym |> ∈-resp-≈)
+      (tag (∈-resp-≈ (≈ˡ-reflexive (insert-lookup γ j A)) w∈⟦e⟧))
+  ... | no i≢j   =
+    0 ,
+      ∈-resp-≈
+        (begin-equality
+          lookup (insert γ i A) j                              ≡˘⟨ cong (lookup (insert γ i A)) (punchIn-punchOut i≢j) ⟩
+          lookup (insert γ i A) (punchIn i (punchOut i≢j))     ≡⟨  insert-punchIn γ i A (punchOut i≢j) ⟩
+          lookup γ (punchOut i≢j)                              ≡˘⟨ insert-punchIn γ i (K 0) (punchOut i≢j) ⟩
+          lookup (insert γ i (K 0)) (punchIn i (punchOut i≢j)) ≡⟨  cong (lookup (insert γ i (K 0))) (punchIn-punchOut i≢j) ⟩
+          lookup (insert γ i (K 0)) j                          ∎)
+        w∈⟦e⟧
+  get-tag (μ e)     A K tag mono i γ {w} (n , w∈⟦e⟧) = map₂ (n ,_) (⟦e⟧′-tag n w∈⟦e⟧)
+    where
+    ⟦e⟧′ : ℕ → Language _ → Language _
+    ⟦e⟧′ n A = Iter (λ X → ⟦ e ⟧ (X ∷ insert γ i A)) ∅ n
+
+    ⟦e⟧′-monoʳ : ∀ n {X Y} → X ⊆ Y → ⟦e⟧′ n X ⊆ ⟦e⟧′ n Y
+    ⟦e⟧′-monoʳ n X⊆Y =
+      Iter-monoˡ
+        (⟦⟧-mono-env e ∘ (_∷ (Pointwise-insert i i {fromWitness refl} X⊆Y (Pw.refl ⊆-refl))))
+        n
+        ⊆-refl
+
+    ⟦e⟧′-tag : ∀ m {w} → w ∈ ⟦e⟧′ m A → ∃[ n ] w ∈ ⟦e⟧′ m (K n)
+    ⟦e⟧′-tag (suc m) {w} w∈⟦e⟧′ =
+      n₁ + n₂ ,
+      ∈-resp-⊆
+        (⟦⟧-mono-env
+          e
+          ( ⟦e⟧′-monoʳ m (mono (m≤m+n n₁ n₂))
+          ∷ Pointwise-insert i i {fromWitness refl} (mono (m≤n+m n₂ n₁)) (Pw.refl ⊆-refl))
+          )
+        w∈⟦e⟧′₂
+      where
+      n₁,w∈⟦e⟧′₁ : ∃[ z ] w ∈ ⟦ e ⟧ (⟦e⟧′ m (K z) ∷ insert γ i A)
+      n₁,w∈⟦e⟧′₁ = get-tag e (⟦e⟧′ m A) (⟦e⟧′ m ∘ K) (⟦e⟧′-tag m) (⟦e⟧′-monoʳ m ∘ mono) zero (insert γ i A) w∈⟦e⟧′
+
+      n₁      = proj₁ n₁,w∈⟦e⟧′₁
+      w∈⟦e⟧′₁ = proj₂ n₁,w∈⟦e⟧′₁
+
+      n₂,w∈⟦e⟧′₂ : ∃[ z ] w ∈ ⟦ e ⟧ (⟦e⟧′ m (K n₁) ∷ insert γ i (K z))
+      n₂,w∈⟦e⟧′₂ = get-tag e A K tag mono (suc i) (⟦e⟧′ m (K n₁) ∷ γ) w∈⟦e⟧′₁
+
+      n₂     = proj₁ n₂,w∈⟦e⟧′₂
+      w∈⟦e⟧′₂ = proj₂ n₂,w∈⟦e⟧′₂
+
+  big-bit : ⟦ e ⟧ (⟦ μ e ⟧ γ ∷ γ) ⊆ ⟦ μ e ⟧ γ
+  big-bit = sub (λ w∈⟦e⟧ →
+    map suc id
+      (get-tag
+        e
+        (⟦ μ e ⟧ γ)
+        (Iter (⟦ e ⟧ ∘ (_∷ γ)) ∅)
+        id
+        (Iter-monoʳ (⟦⟧-mono-env e ∘ (_∷ Pw.refl ⊆-refl)) (⊆-min (⟦ e ⟧ (∅ ∷ γ))))
+        zero
+        γ
+        w∈⟦e⟧))
diff --git a/src/Cfe/Function/Power.agda b/src/Cfe/Function/Power.agda
deleted file mode 100644
index da3b335..0000000
--- a/src/Cfe/Function/Power.agda
+++ /dev/null
@@ -1,37 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module Cfe.Function.Power where
-
-open import Data.Nat using (ℕ)
-open import Data.Product using (∃-syntax; _×_)
-open import Function using (id; _∘_)
-open import Level using (Level; _⊔_)
-open import Relation.Binary using (Rel; REL)
-open import Relation.Binary.PropositionalEquality using (cong; _≡_)
-
-private
-  variable
-    a : Level
-    A : Set a
-
-infix 10 _^_
-
-------------------------------------------------------------------------
--- Definition
-
-_^_ : (A → A) → ℕ → A → A
-f ^ ℕ.zero = id
-f ^ ℕ.suc n = f ∘ f ^ n
-
-------------------------------------------------------------------------
--- Properties
-
-f∼g⇒fⁿ∼gⁿ :
-  ∀ {a b ℓ} {A : Set a} {B : Set b} (_∼_ : REL A B ℓ) {f g 0A 0B} →
-  0A ∼ 0B → (∀ {x y} → x ∼ y → f x ∼ g y) → ∀ n → (f ^ n) 0A ∼ (g ^ n) 0B
-f∼g⇒fⁿ∼gⁿ _ refl ext    ℕ.zero = refl
-f∼g⇒fⁿ∼gⁿ ∼ refl ext (ℕ.suc n) = ext (f∼g⇒fⁿ∼gⁿ ∼ refl ext n)
-
-fⁿf≡fⁿ⁺¹ : ∀ (f : A → A) n → (f ^ n) ∘ f ≡ f ^ (ℕ.suc n)
-fⁿf≡fⁿ⁺¹ f    ℕ.zero = _≡_.refl
-fⁿf≡fⁿ⁺¹ f (ℕ.suc n) = cong (f ∘_) (fⁿf≡fⁿ⁺¹ f n)
diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index d9be456..d73fe19 100644
--- a/src/Cfe/Language/Base.agda
+++ b/src/Cfe/Language/Base.agda
@@ -8,14 +8,14 @@ module Cfe.Language.Base
 
 open Setoid over using () renaming (Carrier to C)
 
-open import Cfe.Function.Power
 open import Data.Empty.Polymorphic using (⊥)
 open import Data.List
 open import Data.List.Relation.Binary.Equality.Setoid over
+open import Data.Nat using (ℕ; zero; suc)
 open import Data.Product
 open import Data.Sum
 open import Function
-open import Level
+open import Level renaming (suc to ℓsuc)
 open import Relation.Binary.PropositionalEquality using (_≡_)
 open import Relation.Nullary using (Dec; ¬_)
 
@@ -26,7 +26,7 @@ private
 ------------------------------------------------------------------------
 -- Definition
 
-record Language a : Set (c ⊔ ℓ ⊔ suc a) where
+record Language a : Set (c ⊔ ℓ ⊔ ℓsuc a) where
   field
     𝕃        : List C → Set a
     ∈-resp-≋ : 𝕃 ⟶ 𝕃 Respects _≋_
@@ -82,11 +82,16 @@ A ∪ B = record
   ; ∈-resp-≋ = uncurry Data.Sum.map ∘ < Language.∈-resp-≋ A , Language.∈-resp-≋ B >
   }
 
+Iter : (Language a → Language a) → Language a → ℕ → Language _
+Iter F A zero    = A
+Iter F A (suc n) = F (Iter F A n)
+
 Sup : (Language a → Language a) → Language a → Language _
 Sup F A = record
-  { 𝕃        = λ w → ∃[ n ] w ∈ (F ^ n) A
-  ; ∈-resp-≋ = λ w≋w′ (n , w∈FⁿA) → n , Language.∈-resp-≋ ((F ^ n) A) w≋w′ w∈FⁿA
+  { 𝕃        = λ w → ∃[ n ] w ∈ Iter F A n
+  ; ∈-resp-≋ = λ w≋w′ (n , w∈FⁿA) → n , Iter.∈-resp-≋ F A n w≋w′ w∈FⁿA
   }
+  where module Iter F A n = Language (Iter F A n)
 
 ⋃_ : (Language a → Language a) → Language _
 ⋃ F = Sup F ∅
@@ -96,7 +101,7 @@ Sup F A = record
 
 infix 4 _⊆_ _≈_
 
-data _⊆_ {a b} : REL (Language a) (Language b) (c ⊔ ℓ ⊔ suc (a ⊔ b)) where
+data _⊆_ {a b} : REL (Language a) (Language b) (c ⊔ ℓ ⊔ ℓsuc (a ⊔ b)) where
   sub : ∀ {A : Language a} {B : Language b} → (∀ {w} → w ∈ A → w ∈ B) → A ⊆ B
 
 _⊇_ : REL (Language a) (Language b) _
diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda
index fe153b1..ca288a8 100644
--- a/src/Cfe/Language/Properties.agda
+++ b/src/Cfe/Language/Properties.agda
@@ -16,7 +16,6 @@ open Setoid over using ()
     )
 
 open import Algebra
-open import Cfe.Function.Power
 open import Cfe.Language.Base over
 open import Cfe.List.Compare over
 open import Data.Empty using (⊥-elim)
@@ -25,11 +24,11 @@ open import Data.List as L
 open import Data.List.Properties
 open import Data.List.Relation.Binary.Equality.Setoid over
 import Data.List.Relation.Unary.Any as Any
-import Data.Nat as ℕ
+open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s)
 open import Data.Product as P
 open import Data.Sum as S
 open import Function hiding (_⟶_)
-open import Level
+open import Level renaming (suc to ℓsuc)
 import Relation.Binary.Construct.On as On
 open import Relation.Binary.PropositionalEquality hiding (setoid; [_])
 open import Relation.Nullary hiding (Irrelevant)
@@ -82,6 +81,12 @@ First-resp-∼ A c∼c′ (w , cw∈A) = w , ∈-resp-≋ (c∼c′ ∷ ≋-refl
 ⊆-min : Min (_⊆_ {a} {b}) ∅
 ⊆-min _ = sub λ ()
 
+⊆-respʳ-≈ : Y ≈ Z → X ⊆ Y → X ⊆ Z
+⊆-respʳ-≈ Y≈Z X⊆Y = ⊆-trans X⊆Y (⊆-reflexive Y≈Z)
+
+⊆-respˡ-≈ : Y ≈ Z → Y ⊆ X → Z ⊆ X
+⊆-respˡ-≈ Y≈Z Y⊆X = ⊆-trans (⊇-reflexive Y≈Z) Y⊆X
+
 ------------------------------------------------------------------------
 -- Membership properties of _⊆_
 
@@ -108,6 +113,9 @@ Flast-resp-⊆ (sub A⊆B) = P.map₂ (P.map₂ (P.map A⊆B (P.map₂ A⊆B)))
 ≈-refl : Reflexive (_≈_ {a})
 ≈-refl = ⊆-refl , ⊆-refl
 
+≈-reflexive : _≡_ ⇒ (_≈_ {a})
+≈-reflexive refl = ≈-refl
+
 ≈-sym : Sym (_≈_ {a} {b}) _≈_
 ≈-sym = P.swap
 
@@ -158,6 +166,93 @@ setoid {a} = record { isEquivalence = ≈-isEquivalence {a} }
 ⊆-poset : ∀ {a} → Poset _ _ _
 ⊆-poset {a} = record { isPartialOrder = ⊆-isPartialOrder {a} }
 
+-- Shamelessly adapted from Relation.Binary.Reasoning.Base.Double
+module ⊆-Reasoning where
+  infix 4 _IsRelatedTo_
+
+  data _IsRelatedTo_ (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ ℓsuc (a ⊔ b)) where
+    nonstrict : (A⊆B : A ⊆ B) → A IsRelatedTo B
+    equals    : (A≈B : A ≈ B) → A IsRelatedTo B
+
+  ------------------------------------------------------------------------
+  -- A record that is used to ensure that the final relation proved by the
+  -- chain of reasoning can be converted into the required relation.
+
+  data IsEquality {A : Language a} {B : Language b} : A IsRelatedTo B → Set (c ⊔ ℓ ⊔ ℓsuc (a ⊔ b)) where
+    isEquality : ∀ A≈B → IsEquality (equals A≈B)
+
+  IsEquality? : ∀ (A⊆B : A IsRelatedTo B) → Dec (IsEquality A⊆B)
+  IsEquality? (nonstrict _) = no λ()
+  IsEquality? (equals A≈B)  = yes (isEquality A≈B)
+
+  extractEquality : ∀ {A⊆B : A IsRelatedTo B} → IsEquality A⊆B → A ≈ B
+  extractEquality (isEquality A≈B) = A≈B
+
+  ------------------------------------------------------------------------
+  -- Reasoning combinators
+
+  -- See `Relation.Binary.Reasoning.Base.Partial` for the design decisions
+  -- behind these combinators.
+
+  infix  1 begin_ begin-equality_
+  infixr 2 step-⊆ step-≈ step-≈˘ step-≡ step-≡˘ _≡⟨⟩_
+  infix  3 _∎
+
+  -- Beginnings of various types of proofs
+
+  begin_ : (r : A IsRelatedTo B) → A ⊆ B
+  begin (nonstrict A⊆B) = A⊆B
+  begin (equals    A≈B) = ⊆-reflexive A≈B
+
+  begin-equality_ : ∀ (r : A IsRelatedTo B) → {s : True (IsEquality? r)} → A ≈ B
+  begin-equality_ r {s} = extractEquality (toWitness s)
+
+  -- Step with the main relation
+
+  step-⊆ : ∀ (X : Language a) → Y IsRelatedTo Z → X ⊆ Y → X IsRelatedTo Z
+  step-⊆ X (nonstrict Y⊆Z) X⊆Y = nonstrict (⊆-trans X⊆Y Y⊆Z)
+  step-⊆ X (equals    Y≈Z) X⊆Y = nonstrict (⊆-respʳ-≈ Y≈Z X⊆Y)
+
+  -- Step with the setoid equality
+
+  step-≈ : ∀ (X : Language a) → Y IsRelatedTo Z → X ≈ Y → X IsRelatedTo Z
+  step-≈ X (nonstrict Y⊆Z) X≈Y = nonstrict (⊆-respˡ-≈ (≈-sym X≈Y) Y⊆Z)
+  step-≈ X (equals    Y≈Z) X≈Y = equals    (≈-trans X≈Y Y≈Z)
+
+  -- Flipped step with the setoid equality
+
+  step-≈˘ : ∀ (X : Language a) → Y IsRelatedTo Z → Y ≈ X → X IsRelatedTo Z
+  step-≈˘ X Y⊆Z Y≈X = step-≈ X Y⊆Z (≈-sym Y≈X)
+
+  -- Step with non-trivial propositional equality
+
+  step-≡ : ∀ (X : Language a) → Y IsRelatedTo Z → X ≡ Y → X IsRelatedTo Z
+  step-≡ X (nonstrict Y⊆Z) X≡Y = nonstrict (case X≡Y of λ { refl → Y⊆Z })
+  step-≡ X (equals    Y≈Z) X≡Y = equals    (case X≡Y of λ { refl → Y≈Z })
+
+  -- Flipped step with non-trivial propositional equality
+
+  step-≡˘ : ∀ (X : Language a) → Y IsRelatedTo Z → Y ≡ X → X IsRelatedTo Z
+  step-≡˘ X Y⊆Z Y≡X = step-≡ X Y⊆Z (sym Y≡X)
+
+  -- Step with trivial propositional equality
+
+  _≡⟨⟩_ : ∀ (X : Language a) → X IsRelatedTo Y → X IsRelatedTo Y
+  X ≡⟨⟩ X⊆Y = X⊆Y
+
+  -- Termination step
+
+  _∎ : ∀ (X : Language a) → X IsRelatedTo X
+  X ∎ = equals ≈-refl
+
+  -- Syntax declarations
+
+  syntax step-⊆  X Y⊆Z X⊆Y = X ⊆⟨  X⊆Y ⟩ Y⊆Z
+  syntax step-≈  X Y⊆Z X≈Y = X ≈⟨  X≈Y ⟩ Y⊆Z
+  syntax step-≈˘ X Y⊆Z Y≈X = X ≈˘⟨ Y≈X ⟩ Y⊆Z
+  syntax step-≡  X Y⊆Z X≡Y = X ≡⟨  X≡Y ⟩ Y⊆Z
+  syntax step-≡˘ X Y⊆Z Y≡X = X ≡˘⟨ Y≡X ⟩ Y⊆Z
+
 ------------------------------------------------------------------------
 -- Membership properties of _≈_
 
@@ -797,26 +892,57 @@ _∪?_ : Decidable A → Decidable B → Decidable (A ∪ B)
 (A? ∪? B?) w = A? w ⊎-dec B? w
 
 ------------------------------------------------------------------------
+-- Properties of Iter
+------------------------------------------------------------------------
+-- Membership properties of Iter
+
+FⁿFA≡Fⁿ⁺¹A : ∀ n → Iter {a} F (F A) n ≡ Iter F A (suc n)
+FⁿFA≡Fⁿ⁺¹A         zero    = refl
+FⁿFA≡Fⁿ⁺¹A {F = F} (suc n) = cong F (FⁿFA≡Fⁿ⁺¹A n)
+
+Iter-monoˡ : (∀ {A B} → A ⊆ B → F A ⊆ G B) → ∀ n → A ⊆ B → Iter F A n ⊆ Iter G B n
+Iter-monoˡ mono zero    A⊆B = A⊆B
+Iter-monoˡ mono (suc n) A⊆B = mono (Iter-monoˡ mono n A⊆B)
+
+Iter-congˡ : (∀ {A B} → A ≈ B → F A ≈ G B) → ∀ n → A ≈ B → Iter F A n ≈ Iter G B n
+Iter-congˡ cong zero    A≈B = A≈B
+Iter-congˡ cong (suc n) A≈B = cong (Iter-congˡ cong n A≈B)
+
+Iter-step : (∀ {A B} → A ⊆ B → F A ⊆ F B) → A ⊆ F A → ∀ n → Iter F A n ⊆ Iter F A (suc n)
+Iter-step mono A⊆FA zero    = A⊆FA
+Iter-step mono A⊆FA (suc n) = mono (Iter-step mono A⊆FA n)
+
+Iter-monoʳ : (∀ {A B} → A ⊆ B → F A ⊆ F B) → A ⊆ F A → ∀ {m n} → m ≤ n → Iter F A m ⊆ Iter F A n
+Iter-monoʳ                 mono A⊆FA {n = zero}  z≤n       = ⊆-refl
+Iter-monoʳ {F = F} {A = A} mono A⊆FA {n = suc n} z≤n       = begin
+  A              ⊆⟨ A⊆FA ⟩
+  F A            ⊆⟨ mono (Iter-monoʳ mono A⊆FA {n = n} z≤n) ⟩
+  F (Iter F A n) ∎
+  where open ⊆-Reasoning
+Iter-monoʳ                 mono A⊆FA             (s≤s m≤n) = mono (Iter-monoʳ mono A⊆FA m≤n)
+
+------------------------------------------------------------------------
 -- Properties of Sup
 ------------------------------------------------------------------------
 -- Membership properties of Sup
 
-FⁿA⊆SupFA : ∀ n → (F ^ n) A ⊆ Sup F A
+FⁿA⊆SupFA : ∀ n → Iter F A n ⊆ Sup F A
 FⁿA⊆SupFA n = sub (n ,_)
 
-FⁿFA⊆SupFA : ∀ n → (F ^ n) (F A) ⊆ Sup F A
-FⁿFA⊆SupFA {F = F} {A = A} n = ⊆-trans (sub (go n)) (FⁿA⊆SupFA (ℕ.suc n))
-  where
-  go : ∀ {w} n → w ∈ (F ^ n) (F A) → w ∈ (F ^ (ℕ.suc n)) A
-  go {w = w} n w∈Fⁿ̂FA = subst (λ x → w ∈ x A) (fⁿf≡fⁿ⁺¹ F n) w∈Fⁿ̂FA
+FⁿFA⊆SupFA : ∀ n → Iter F (F A) n ⊆ Sup F A
+FⁿFA⊆SupFA {F = F} {A = A} n = begin
+  Iter F (F A) n   ≡⟨ FⁿFA≡Fⁿ⁺¹A n ⟩
+  Iter F A (suc n) ⊆⟨ FⁿA⊆SupFA (suc n) ⟩
+  Sup F A          ∎
+  where open ⊆-Reasoning
 
-∀[FⁿA⊆B]⇒SupFA⊆B : (∀ n → (F ^ n) A ⊆ B) → Sup F A ⊆ B
+∀[FⁿA⊆B]⇒SupFA⊆B : (∀ n → Iter F A n ⊆ B) → Sup F A ⊆ B
 ∀[FⁿA⊆B]⇒SupFA⊆B FⁿA⊆B = sub λ (n , w∈FⁿA) → ∈-resp-⊆ (FⁿA⊆B n) w∈FⁿA
 
-∃[B⊆FⁿA]⇒B⊆SupFA : ∀ n → B ⊆ (F ^ n) A → B ⊆ Sup F A
+∃[B⊆FⁿA]⇒B⊆SupFA : ∀ n → B ⊆ Iter F A n → B ⊆ Sup F A
 ∃[B⊆FⁿA]⇒B⊆SupFA n B⊆FⁿA = sub λ w∈B → n , ∈-resp-⊆ B⊆FⁿA w∈B
 
-∀[FⁿA≈GⁿB]⇒SupFA≈SupGB : (∀ n → (F ^ n) A ≈ (G ^ n) B) → Sup F A ≈ Sup G B
+∀[FⁿA≈GⁿB]⇒SupFA≈SupGB : (∀ n → Iter F A n ≈ Iter G B n) → Sup F A ≈ Sup G B
 ∀[FⁿA≈GⁿB]⇒SupFA≈SupGB FⁿA≈GⁿB =
   ⊆-antisym
     (sub λ (n , w∈FⁿA) → n , ∈-resp-≈ (FⁿA≈GⁿB n) w∈FⁿA)
@@ -826,34 +952,38 @@ FⁿFA⊆SupFA {F = F} {A = A} n = ⊆-trans (sub (go n)) (FⁿA⊆SupFA (ℕ.su
 ------------------------------------------------------------------------
 -- Membership properties of ⋃_
 
-Fⁿ⊆⋃F : ∀ n → (F ^ n) ∅ ⊆ ⋃ F
+Fⁿ⊆⋃F : ∀ n → Iter F ∅ n ⊆ ⋃ F
 Fⁿ⊆⋃F = FⁿA⊆SupFA
 
-∀[Fⁿ⊆B]⇒⋃F⊆B : (∀ n → (F ^ n) ∅ ⊆ B) → ⋃ F ⊆ B
+∀[Fⁿ⊆B]⇒⋃F⊆B : (∀ n → Iter F ∅ n ⊆ B) → ⋃ F ⊆ B
 ∀[Fⁿ⊆B]⇒⋃F⊆B = ∀[FⁿA⊆B]⇒SupFA⊆B
 
-∃[B⊆Fⁿ]⇒B⊆⋃F : ∀ n → B ⊆ (F ^ n) ∅ → B ⊆ ⋃ F
+∃[B⊆Fⁿ]⇒B⊆⋃F : ∀ n → B ⊆ Iter F ∅ n → B ⊆ ⋃ F
 ∃[B⊆Fⁿ]⇒B⊆⋃F = ∃[B⊆FⁿA]⇒B⊆SupFA
 
-∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G : (∀ n → (F ^ n) ∅ ≈ (G ^ n) ∅) → ⋃ F ≈ ⋃ G
+∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G : (∀ n → Iter F ∅ n ≈ Iter G ∅ n) → ⋃ F ≈ ⋃ G
 ∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G = ∀[FⁿA≈GⁿB]⇒SupFA≈SupGB
 
 ------------------------------------------------------------------------
 -- Functional properties of ⋃_
 
 ⋃-mono : (∀ {A B} → A ⊆ B → F A ⊆ G B) → ⋃ F ⊆ ⋃ G
-⋃-mono mono-ext = ∀[Fⁿ⊆B]⇒⋃F⊆B λ n → ⊆-trans (f∼g⇒fⁿ∼gⁿ _⊆_ (⊆-min ∅) mono-ext n) (Fⁿ⊆⋃F n)
+⋃-mono {F = F} {G = G} mono-ext = ∀[Fⁿ⊆B]⇒⋃F⊆B λ n → (begin
+  Iter F ∅ n ⊆⟨ Iter-monoˡ mono-ext n (⊆-min ∅) ⟩
+  Iter G ∅ n ⊆⟨ Fⁿ⊆⋃F n ⟩
+  ⋃ G        ∎)
+  where open ⊆-Reasoning
 
 ⋃-cong : (∀ {A B} → A ≈ B → F A ≈ G B) → ⋃ F ≈ ⋃ G
-⋃-cong ext = ∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G (f∼g⇒fⁿ∼gⁿ _≈_ (⊆-antisym (⊆-min ∅) (⊆-min ∅)) ext)
+⋃-cong ext = ∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G λ n → Iter-congˡ ext n (⊆-antisym (⊆-min ∅) (⊆-min ∅))
 
 ⋃-inverseʳ : ∀ (A : Language a) → ⋃ (const A) ≈ A
-⋃-inverseʳ _ = ⊆-antisym (sub λ {(ℕ.suc _ , w∈A) → w∈A}) (Fⁿ⊆⋃F 1)
+⋃-inverseʳ _ = ⊆-antisym (sub λ {(suc _ , w∈A) → w∈A}) (Fⁿ⊆⋃F 1)
 
 ⋃-unroll : (∀ {A B} → A ⊆ B → F A ⊆ F B) → ⋃ F ⊆ F (⋃ F)
 ⋃-unroll {F = F} mono-ext = ∀[Fⁿ⊆B]⇒⋃F⊆B λ
-  { ℕ.zero    → ⊆-min (F (⋃ F))
-  ; (ℕ.suc n) → mono-ext (Fⁿ⊆⋃F n)
+  { zero    → ⊆-min (F (⋃ F))
+  ; (suc n) → mono-ext (Fⁿ⊆⋃F n)
   }
 
 ------------------------------------------------------------------------
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index 21051c0..4b38c1e 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -16,7 +16,6 @@ open Setoid over using ()
   )
 
 open import Algebra
-open import Cfe.Function.Power
 open import Cfe.Language over
   hiding
   ( _≉_; ≈-refl; ≈-trans; ≈-isPartialEquivalence; ≈-isEquivalence; partialSetoid; setoid
@@ -356,19 +355,20 @@ setoid {fℓ} {lℓ} = record { isEquivalence = ≈-isEquivalence {fℓ} {lℓ}
   ; l⇒l = λ (x , w , (m , xw∈Fᵐ) , w′ , n , xwcw′∈Fⁿ) →
     Fⁿ⊨τ.l⇒l
       (m + n)
-      (-, -, ∈-resp-⊆ (step (m≤m+n m n)) xw∈Fᵐ , -, ∈-resp-⊆ (step (m≤n+m n m)) xwcw′∈Fⁿ)
+      ( x
+      , w
+      , ∈-resp-⊆ (Iter-monoʳ mono (⊆-min (F ∅)) (m≤m+n m n)) xw∈Fᵐ
+      , w′
+      , ∈-resp-⊆ (Iter-monoʳ mono (⊆-min (F ∅)) (m≤n+m n m)) xwcw′∈Fⁿ
+      )
   }
   where
-  Fⁿ⊨τ : ∀ n → (F ^ n) ∅ ⊨ τ
+  Fⁿ⊨τ : ∀ n → Iter F ∅ n ⊨ τ
   Fⁿ⊨τ zero    = ⊨-min τ
   Fⁿ⊨τ (suc n) = ⊨-step (Fⁿ⊨τ n)
 
   module Fⁿ⊨τ n = _⊨_ (Fⁿ⊨τ n)
 
-  step : ∀ {m n} → m ≤ⁿ n → (F ^ m) ∅ ⊆ (F ^ n) ∅
-  step {n = n} z≤n       = ⊆-min ((F  ^ n) ∅)
-  step         (s≤s m≤n) = mono (step m≤n)
-
 ------------------------------------------------------------------------
 -- Properties of _⊛_
 ------------------------------------------------------------------------
diff --git a/src/Cfe/Vec/Relation/Binary/Pointwise/Inductive.agda b/src/Cfe/Vec/Relation/Binary/Pointwise/Inductive.agda
new file mode 100644
index 0000000..ba75606
--- /dev/null
+++ b/src/Cfe/Vec/Relation/Binary/Pointwise/Inductive.agda
@@ -0,0 +1,41 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Cfe.Vec.Relation.Binary.Pointwise.Inductive where
+
+open import Data.Fin using (toℕ; zero; suc)
+open import Data.Nat using (ℕ; suc; _≟_; pred)
+open import Data.Vec using (Vec; insert; remove)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
+open import Function using (_|>_)
+open import Level using (Level)
+open import Relation.Binary using (REL; Antisym)
+open import Relation.Binary.PropositionalEquality using (cong)
+open import Relation.Nullary.Decidable using (True; toWitness; fromWitness)
+
+private
+  variable
+    a b ℓ : Level
+    A : Set a
+    B : Set b
+    _∼_ : REL A B ℓ
+    m n : ℕ
+
+antisym :
+  ∀ {P : REL A B ℓ} {Q : REL B A ℓ} {R : REL A B ℓ} →
+  Antisym P Q R → Antisym (Pointwise P {m} {n}) (Pointwise Q) (Pointwise R)
+antisym anti []       []       = []
+antisym anti (x ∷ xs) (y ∷ ys) = anti x y ∷ antisym anti xs ys
+
+Pointwise-insert :
+  ∀ {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)
+Pointwise-insert zero    zero          x xs       = x ∷ xs
+Pointwise-insert (suc i) (suc j) {i≡j} x (y ∷ xs) =
+  y ∷ Pointwise-insert i j {i≡j |> toWitness |> cong pred |> fromWitness} x xs
+
+Pointwise-remove :
+  ∀ {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)
+Pointwise-remove zero zero (_ ∷ xs) = xs
+Pointwise-remove (suc i) (suc j) {i≡j} (x ∷ y ∷ xs) =
+  x ∷ Pointwise-remove i j {i≡j |> toWitness |> cong pred |> fromWitness} (y ∷ xs)