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

Complete proof of generator.

2 files changed, 208 insertions, 61 deletions

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⟧))