Cleanup Derivation.cleanup

4 files changed, 122 insertions, 124 deletions

diff --git a/src/Cfe/Derivation/Base.agda b/src/Cfe/Derivation/Base.agda
index ce368d0..0432c3d 100644
--- a/src/Cfe/Derivation/Base.agda
+++ b/src/Cfe/Derivation/Base.agda
@@ -8,37 +8,41 @@ module Cfe.Derivation.Base
 
 open Setoid over renaming (Carrier to C; _≈_ to _∼_)
 
-open import Cfe.Expression over hiding (_≋_)
-open import Data.Fin
-open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid over
+open import Cfe.Expression over hiding (_≈_)
+open import Data.Fin using (zero)
+open import Data.List using (List; []; [_]; _++_)
+open import Data.List.Relation.Binary.Equality.Setoid over using (_≋_)
 open import Level using (_⊔_)
 
 infix 5 _⤇_
 infix 4 _≈_
 
 data _⤇_ : Expression 0 → List C → Set (c ⊔ ℓ) where
-  Eps : ε ⤇ []
+  Eps  : ε ⤇ []
   Char : ∀ {c y} → (c∼y : c ∼ y) → Char c ⤇ [ y ]
-  Cat : ∀ {e₁ e₂ l₁ l₂ l} → e₁ ⤇ l₁ → e₂ ⤇ l₂ → l₁ ++ l₂ ≋ l → e₁ ∙ e₂ ⤇ l
-  Veeˡ : ∀ {e₁ e₂ l} → e₁ ⤇ l → e₁ ∨ e₂ ⤇ l
-  Veeʳ : ∀ {e₁ e₂ l} → e₂ ⤇ l → e₁ ∨ e₂ ⤇ l
-  Fix : ∀ {e l} → e [ μ e / zero ] ⤇ l → μ e ⤇ l
+  Cat  : ∀ {e₁ e₂ w₁ w₂ w} → e₁ ⤇ w₁ → e₂ ⤇ w₂ → w₁ ++ w₂ ≋ w → e₁ ∙ e₂ ⤇ w
+  Veeˡ : ∀ {e₁ e₂ w} → e₁ ⤇ w → e₁ ∨ e₂ ⤇ w
+  Veeʳ : ∀ {e₁ e₂ w} → e₂ ⤇ w → e₁ ∨ e₂ ⤇ w
+  Fix  : ∀ {e w} → e [ μ e / zero ] ⤇ w → μ e ⤇ w
 
-data _≈_ : ∀ {e l l′} → REL (e ⤇ l) (e ⤇ l′) (c ⊔ ℓ) where
-  Eps : Eps ≈ Eps
+data _≈_ : ∀ {e w w′} → REL (e ⤇ w) (e ⤇ w′) (c ⊔ ℓ) where
+  Eps  : Eps ≈ Eps
   Char : ∀ {c y y′} → (c∼y : c ∼ y) → (c∼y′ : c ∼ y′) → Char c∼y ≈ Char c∼y′
-  Cat : ∀ {e₁ e₂ l l₁ l₂ l₁′ l₂′ e₁⤇l₁ e₁⤇l₁′ e₂⤇l₂ e₂⤇l₂′} →
-          (e₁⤇l₁≈e₁⤇l′ : _≈_ {e₁} {l₁} {l₁′} e₁⤇l₁ e₁⤇l₁′) →
-          (e₂⤇l₂≈e₂⤇l′ : _≈_ {e₂} {l₂} {l₂′} e₂⤇l₂ e₂⤇l₂′) →
-          (eq : l₁ ++ l₂ ≋ l) → (eq′ : l₁′ ++ l₂′ ≋ l) →
-          Cat e₁⤇l₁ e₂⤇l₂ eq ≈ Cat e₁⤇l₁′ e₂⤇l₂′ eq′
-  Veeˡ : ∀ {e₁ e₂ l l′ e₁⤇l e₁⤇l′} →
-         (e₁⤇l≈e₁⤇l′ : _≈_ {e₁} {l} {l′} e₁⤇l e₁⤇l′) →
-         Veeˡ {e₂ = e₂} e₁⤇l ≈ Veeˡ e₁⤇l′
-  Veeʳ : ∀ {e₁ e₂ l l′ e₂⤇l e₂⤇l′} →
-         (e₂⤇l≈e₂⤇l′ : _≈_ {e₂} {l} {l′} e₂⤇l e₂⤇l′) →
-         Veeʳ {e₁} e₂⤇l ≈ Veeʳ e₂⤇l′
-  Fix : ∀ {e l l′ e[μe/0]⤇l e[μe/0]⤇l′} →
-        (e[μe/0]⤇l≈e[μe/0]⤇l′ : _≈_ {e [ μ e / zero ]} {l} {l′} e[μe/0]⤇l e[μe/0]⤇l′) →
-        Fix {e} e[μe/0]⤇l ≈ Fix e[μe/0]⤇l′
+  Cat  :
+    ∀ {e₁ e₂ w w₁ w₂ w₁′ w₂′ e₁⤇w₁ e₁⤇w₁′ e₂⤇w₂ e₂⤇w₂′} →
+    (e₁⤇w₁≈e₁⤇w′ : _≈_ {e₁} {w₁} {w₁′} e₁⤇w₁ e₁⤇w₁′) →
+    (e₂⤇w₂≈e₂⤇w′ : _≈_ {e₂} {w₂} {w₂′} e₂⤇w₂ e₂⤇w₂′) →
+    (eq : w₁ ++ w₂ ≋ w) → (eq′ : w₁′ ++ w₂′ ≋ w) →
+    Cat e₁⤇w₁ e₂⤇w₂ eq ≈ Cat e₁⤇w₁′ e₂⤇w₂′ eq′
+  Veeˡ :
+    ∀ {e₁ e₂ w w′ e₁⤇w e₁⤇w′} →
+    (e₁⤇w≈e₁⤇w′ : _≈_ {e₁} {w} {w′} e₁⤇w e₁⤇w′) →
+    Veeˡ {e₂ = e₂} e₁⤇w ≈ Veeˡ e₁⤇w′
+  Veeʳ :
+    ∀ {e₁ e₂ w w′ e₂⤇w e₂⤇w′} →
+    (e₂⤇w≈e₂⤇w′ : _≈_ {e₂} {w} {w′} e₂⤇w e₂⤇w′) →
+    Veeʳ {e₁} e₂⤇w ≈ Veeʳ e₂⤇w′
+  Fix  :
+    ∀ {e w w′ e[μe/0]⤇w e[μe/0]⤇w′} →
+    (e[μe/0]⤇w≈e[μe/0]⤇w′ : _≈_ {e [ μ e / zero ]} {w} {w′} e[μe/0]⤇w e[μe/0]⤇w′) →
+    Fix {e} e[μe/0]⤇w ≈ Fix e[μe/0]⤇w′
diff --git a/src/Cfe/Derivation/Properties.agda b/src/Cfe/Derivation/Properties.agda
index e89d9f1..d922f2a 100644
--- a/src/Cfe/Derivation/Properties.agda
+++ b/src/Cfe/Derivation/Properties.agda
@@ -6,111 +6,69 @@ module Cfe.Derivation.Properties
   {c ℓ} (over : Setoid c ℓ)
   where
 
-open Setoid over renaming (Carrier to C; _≈_ to _∼_)
+open Setoid over using () renaming (Carrier to C)
 
-open import Cfe.Context over hiding (_≋_)
-open import Cfe.Expression over hiding (_≋_)
-open import Cfe.Language over hiding (≤-refl; _≈_; _<_)
-open import Cfe.Language.Construct.Concatenate over using (Concat)
-open import Cfe.Language.Indexed.Construct.Iterate over
-open import Cfe.Judgement over
+open import Cfe.Context over using (∙,∙)
 open import Cfe.Derivation.Base over
+open import Cfe.Expression over
+open import Cfe.Fin using (zero)
+open import Cfe.Judgement over
+open import Cfe.Language over hiding (_∙_)
 open import Cfe.Type over using (_⊛_; _⊨_)
-open import Data.Bool using (T; not; true; false)
-open import Data.Empty using (⊥-elim)
-open import Data.Fin as F hiding (_<_)
-open import Data.List hiding (null)
-open import Data.List.Relation.Binary.Equality.Setoid over
-open import Data.Nat as ℕ hiding (_⊔_; _^_; _<_)
-open import Data.Nat.Properties using (≤-step; m≤m+n; m≤n+m; ≤-refl; n<1+n; module ≤-Reasoning)
-open import Data.Nat.Induction using () renaming (<-wellFounded to <ⁿ-wellFounded)
-open import Data.Product as Product
-open import Data.Product.Relation.Binary.Lex.Strict
-open import Data.Sum as Sum
-open import Data.Vec hiding (length; _++_)
-open import Data.Vec.Relation.Binary.Pointwise.Inductive
-open import Data.Vec.Relation.Binary.Pointwise.Extensional
-open import Function
+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 Induction.WellFounded
-open import Level
-open import Relation.Binary
-import Relation.Binary.Construct.On as On
-open import Relation.Binary.PropositionalEquality as ≡ hiding (subst₂; setoid)
-
-private
-  infix 4 _<_
-  _<_ : Rel (List C × Expression 0) _
-  _<_ = ×-Lex _≡_ ℕ._<_ _<ᵣₐₙₖ_ on (Product.map₁ length)
+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 (¬_)
 
-  <-wellFounded : WellFounded _<_
-  <-wellFounded = On.wellFounded (Product.map₁ length) (×-wellFounded <ⁿ-wellFounded <ᵣₐₙₖ-wellFounded)
-
-l∈⟦e⟧⇒e⤇l : ∀ {e τ} → ∙,∙ ⊢ e ∶ τ → ∀ {l} → l ∈ ⟦ e ⟧ [] → e ⤇ l
-l∈⟦e⟧⇒e⤇l {e} {τ} ∙,∙⊢e∶τ {l} l∈⟦e⟧ = All.wfRec <-wellFounded _ Pred go (l , e) ∙,∙⊢e∶τ l∈⟦e⟧
+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⟧
   where
-  Pred : List C × Expression 0 → Set _
-  Pred (l , e) = ∀ {τ} → ∙,∙ ⊢ e ∶ τ → l ∈ ⟦ e ⟧ [] → e ⤇ l
-
-  e[μe/0]<μe : ∀ {e τ} l → ∙,∙ ⊢ μ e ∶ τ → (l , e [ μ e / F.zero ]) < (l , μ e)
-  e[μe/0]<μe {e} l (Fix ∙,τ⊢e∶τ)= inj₂ (≡.refl , (begin-strict
-    rank (e [ μ e / F.zero ]) ≡⟨ subst-preserves-rank z≤n ∙,τ⊢e∶τ (Fix ∙,τ⊢e∶τ) ⟩
-    rank e                    <⟨ n<1+n (rank e) ⟩
-    ℕ.suc (rank e)            ≡⟨⟩
-    rank (μ e)                ∎))
-    where
-    open ≤-Reasoning
+  Pred : (List C × Expression 0) → Set _
+  Pred (w , e) = ∀ {τ} → ∙,∙ ⊢ e ∶ τ → w ∈ ⟦ e ⟧ [] → e ⤇ w
 
-  l₁++l₂≋l⇒∣l₁∣≤∣l∣ : ∀ {l₂ l} l₁ → l₁ ++ l₂ ≋ l → (length l₁ ℕ.< length l) ⊎ (length l₁ ≡ length l)
-  l₁++l₂≋l⇒∣l₁∣≤∣l∣ [] [] = inj₂ ≡.refl
-  l₁++l₂≋l⇒∣l₁∣≤∣l∣ [] (_ ∷ _) = inj₁ (s≤s z≤n)
-  l₁++l₂≋l⇒∣l₁∣≤∣l∣ (_ ∷ l₁) (_ ∷ eq) = Sum.map s≤s (cong ℕ.suc) (l₁++l₂≋l⇒∣l₁∣≤∣l∣ l₁ eq)
-
-  l₁++l₂≋l⇒∣l₂∣≤∣l∣ : ∀ {l₂ l} l₁ → l₁ ++ l₂ ≋ l → (length l₂ ℕ.< length l) ⊎ (length l₁ ≡ 0)
-  l₁++l₂≋l⇒∣l₂∣≤∣l∣ [] _ = inj₂ ≡.refl
-  l₁++l₂≋l⇒∣l₂∣≤∣l∣ (_ ∷ []) (_ ∷ []) = inj₁ (s≤s z≤n)
-  l₁++l₂≋l⇒∣l₂∣≤∣l∣ (x ∷ []) (x∼y ∷ _ ∷ eq) = inj₁ ([ s≤s , (λ ()) ]′ (l₁++l₂≋l⇒∣l₂∣≤∣l∣ (x ∷ []) (x∼y ∷ eq)))
-  l₁++l₂≋l⇒∣l₂∣≤∣l∣ (_ ∷ x ∷ l₁) (_ ∷ eq) = inj₁ ([ ≤-step , (λ ()) ]′ (l₁++l₂≋l⇒∣l₂∣≤∣l∣ (x ∷ l₁) eq))
-
-  e₁<e₁∙e₂ : ∀ {l e₁} e₂ → (l∈⟦e₁∙e₂⟧ : l ∈ ⟦ e₁ ∙ e₂ ⟧ []) → (Concat.l₁ l∈⟦e₁∙e₂⟧ , e₁) < (l , e₁ ∙ e₂)
-  e₁<e₁∙e₂ _ l∈⟦e₁∙e₂⟧ with l₁++l₂≋l⇒∣l₁∣≤∣l∣ (Concat.l₁ l∈⟦e₁∙e₂⟧) (Concat.eq l∈⟦e₁∙e₂⟧)
-  ... | inj₁ ∣l₁∣<∣l∣ = inj₁ ∣l₁∣<∣l∣
-  ... | inj₂ ∣l₁∣≡∣l∣ = inj₂ (∣l₁∣≡∣l∣ , ≤-refl)
-
-  e₂<e₁∙e₂ : ∀ {l e₁ e₂ τ} → ∙,∙ ⊢ e₁ ∙ e₂ ∶ τ → (l∈⟦e₁∙e₂⟧ : l ∈ ⟦ e₁ ∙ e₂ ⟧ []) → (Concat.l₂ l∈⟦e₁∙e₂⟧ , e₂) < (l , e₁ ∙ e₂)
-  e₂<e₁∙e₂ (Cat ∙,∙⊢e₁∶τ₁ _ τ₁⊛τ₂) l∈⟦e₁∙e₂⟧ with l₁++l₂≋l⇒∣l₂∣≤∣l∣ (Concat.l₁ l∈⟦e₁∙e₂⟧) (Concat.eq l∈⟦e₁∙e₂⟧)
-  ... | inj₁ ∣l₂∣<∣l∣ = inj₁ ∣l₂∣<∣l∣
-  ... | inj₂ ∣l₁∣≡0 with Concat.l₁ l∈⟦e₁∙e₂⟧ | Concat.l₁∈A l∈⟦e₁∙e₂⟧ | (_⊛_.τ₁.Null τ₁⊛τ₂) | _⊛_.¬n₁ τ₁⊛τ₂ | _⊨_.n⇒n (soundness ∙,∙⊢e₁∶τ₁ [] (ext (λ ()))) | ∣l₁∣≡0
-  ... | [] | ε∈A | false | _ | n⇒n | refl = ⊥-elim (n⇒n ε∈A)
-
-  l∈⟦e⟧ⁿ⇒l∈⟦e[μe/0]⟧ : ∀ {l} e n → l ∈ ((λ X → ⟦ e ⟧ (X ∷ [])) ^ n) (⟦ ⊥ ⟧ []) → l ∈ ⟦ e [ μ e / F.zero ] ⟧ []
-  l∈⟦e⟧ⁿ⇒l∈⟦e[μe/0]⟧ e (suc n) l∈⟦e⟧ⁿ = _≤_.f
-    (begin
-      ((λ X → ⟦ e ⟧ (X ∷ [])) ^ (ℕ.suc n)) (⟦ ⊥ ⟧ [])      ≡⟨⟩
-      ⟦ e ⟧ (((λ X → ⟦ e ⟧ (X ∷ [])) ^ n) (⟦ ⊥ ⟧ []) ∷ []) ≤⟨ mono e (fⁿ≤⋃f (λ X → ⟦ e ⟧ (X ∷ [])) n ∷ []) ⟩
-      ⟦ e ⟧ (⋃ (λ X → ⟦ e ⟧ (X ∷ [])) ∷ [])                ≡⟨⟩
-      ⟦ e ⟧ (⟦ μ e ⟧ [] ∷ [])                              ≈˘⟨ subst-fun e (μ e) F.zero [] ⟩
-      ⟦ e [ μ e / F.zero ] ⟧ []                            ∎)
-    l∈⟦e⟧ⁿ
+  go : ∀ w,e → WfRec _<ₗₑₓ_ Pred w,e → Pred w,e
+  go ([] , ε)       rec Eps      w∈⟦e⟧      = Eps
+  go (w  , Char c)  rec (Char c) (c∼y ∷ []) = Char c∼y
+  go (w  , μ e)     rec (Fix ctx⊢e∶τ) w∈⟦e⟧ =
+    Fix (rec
+      (w , e [ μ e / zero ])
+      w,e[μe/0]<ₗₑₓw,μe
+      (subst₂ ctx⊢e∶τ zero (Fix ctx⊢e∶τ))
+      (∈-resp-⊆ ⟦μe⟧⊆⟦e[μe/0]⟧ w∈⟦e⟧))
     where
-    open import Relation.Binary.Reasoning.PartialOrder (poset _)
+    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
 
-  go : ∀ l,e → WfRec _<_ Pred l,e → Pred l,e
-  go (l , e) rec Eps (lift refl) = Eps
-  go (l , e) rec (Char c) (lift (c∼y ∷ [])) = Char c∼y
-  go (l , μ e) rec (Fix ∙,τ⊢e∶τ) (n , l∈⟦e⟧ⁿ) =
-    Fix (rec
-      (l , e [ μ e / F.zero ])
-      (e[μe/0]<μe l (Fix ∙,τ⊢e∶τ))
-      (subst₂ z≤n ∙,τ⊢e∶τ (Fix ∙,τ⊢e∶τ))
-      (l∈⟦e⟧ⁿ⇒l∈⟦e[μe/0]⟧ e n l∈⟦e⟧ⁿ))
-  go (l , e₁ ∙ e₂) rec (∙,∙⊢e₁∙e₂∶τ @ (Cat ∙,∙⊢e₁∶τ₁ ∙,∙⊢e₂∶τ₂ _)) l∈⟦e⟧ =
+    ⟦μ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 [ μ e / zero ] ⟧ [] ∎
+      where open ⊆-Reasoning
+  go (w  , e₁ ∙ e₂) rec (Cat ctx⊢e₁∶τ₁ ctx⊢e₂∶τ₂ τ₁⊛τ₂) (w₁ , w₂ , w₁∈⟦e₁⟧ , w₂∈⟦e₂⟧ , eq) =
     Cat
-      (rec (l∈⟦e⟧.l₁ , e₁) (e₁<e₁∙e₂ e₂ l∈⟦e⟧) ∙,∙⊢e₁∶τ₁ l∈⟦e⟧.l₁∈A)
-      (rec (l∈⟦e⟧.l₂ , e₂) (e₂<e₁∙e₂ ∙,∙⊢e₁∙e₂∶τ  l∈⟦e⟧) ∙,∙⊢e₂∶τ₂ l∈⟦e⟧.l₂∈B)
-      l∈⟦e⟧.eq
+      (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₂⟧)
+      eq
     where
-    module l∈⟦e⟧ = Concat l∈⟦e⟧
-  go (l , e₁ ∨ e₂) rec (Vee ∙,∙⊢e₁∶τ₁ _ _) (inj₁ l∈⟦e₁⟧) =
-    Veeˡ (rec (l , e₁) (inj₂ (≡.refl , e₁<ᵣₐₙₖe₁∨e₂ e₁ e₂)) ∙,∙⊢e₁∶τ₁ l∈⟦e₁⟧)
-  go (l , e₁ ∨ e₂) rec (Vee _ ∙,∙⊢e₂∶τ₂ _) (inj₂ l∈⟦e₂⟧) =
-    Veeʳ (rec (l , e₂) (inj₂ (≡.refl , e₂<ᵣₐₙₖe₁∨e₂ e₁ e₂)) ∙,∙⊢e₂∶τ₂ l∈⟦e₂⟧)
+    open _⊛_ τ₁⊛τ₂ using (¬n₁)
+    ε∉⟦e₁⟧ : ¬ Null (⟦ e₁ ⟧ [])
+    ε∉⟦e₁⟧ = ¬n₁ ∘ _⊨_.n⇒n (soundness ctx⊢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₁⟧)
+  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₂⟧)
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
index 40d569a..d994fe6 100644
--- a/src/Cfe/Expression/Properties.agda
+++ b/src/Cfe/Expression/Properties.agda
@@ -39,14 +39,18 @@ open import Data.List using (List; length; _++_)
 open import Data.List.Properties using (length-++)
 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.Vec.Properties
 open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
   hiding (refl; sym; trans; setoid; lookup)
+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
 
@@ -154,6 +158,16 @@ _<ₗₑₓ_ : REL (List C × Expression m) (List C × Expression n) _
 <ₗₑₓ-asym (inj₂ (_ , r₁<r₂))      (inj₂ (_ , r₂<r₁))    = <ᵣₐₙₖ-asym r₁<r₂ r₂<r₁
 
 ------------------------------------------------------------------------
+-- Induction properties
+
+<ᵣₐₙₖ-wellFounded : WellFounded (_<ᵣₐₙₖ_ {n})
+<ᵣₐₙₖ-wellFounded = on-wellFounded rank <-wellFounded
+
+<ₗₑₓ-wellFounded : WellFounded (_<ₗₑₓ_ {n})
+<ₗₑₓ-wellFounded = on-wellFounded (map₁ length) (×-wellFounded <-wellFounded <ᵣₐₙₖ-wellFounded)
+
+
+------------------------------------------------------------------------
 -- Other properties
 
 rank-∨ˡ : ∀ (e₁ e₂ : Expression n) → e₁ <ᵣₐₙₖ e₁ ∨ e₂
@@ -175,6 +189,23 @@ rank-∨ʳ e₁ e₂ = begin-strict
 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∣
+  where
+  open ≤-Reasoning
+  ∣w₁∣≤∣w∣ : length w₁ ≤ length w
+  ∣w₁∣≤∣w∣ = begin
+    length w₁             ≤⟨ m≤m+n (length w₁) (length w₂) ⟩
+    length w₁ + length w₂ ≡˘⟨ length-++ w₁ ⟩
+    length (w₁ ++ w₂)     ≡⟨ Pointwise-length eq ⟩
+    length w              ∎
+... | inj₁ ∣w₁∣<∣w∣ = inj₁ ∣w₁∣<∣w∣
+... | inj₂ ∣w₁∣≡∣w∣ = inj₂ (∣w₁∣≡∣w∣ , rank-∙ˡ e₁ e₂)
+
 lex-∙ʳ :
   ∀ (e₁ e₂ : Expression n) γ → ¬ Null (⟦ e₁ ⟧ γ) →
   ∀ {w} → (w∈⟦e₁∙e₂⟧ : w ∈ ⟦ e₁ ∙ e₂ ⟧ γ) →
@@ -182,14 +213,13 @@ lex-∙ʳ :
   (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∣
   where
+  open ≤-Reasoning
   ∣w₂∣≤∣w∣ : length w₂ ≤ length w
   ∣w₂∣≤∣w∣ = begin
     length w₂             ≤⟨ m≤n+m (length w₂) (length w₁) ⟩
     length w₁ + length w₂ ≡˘⟨ length-++ w₁ ⟩
     length (w₁ ++ w₂)     ≡⟨ Pointwise-length eq ⟩
     length w              ∎
-    where
-    open ≤-Reasoning
 ... | inj₁ ∣w₂∣<∣w∣ = inj₁ ∣w₂∣<∣w∣
 ... | inj₂ ∣w₂∣≡∣w∣ = ⊥-elim (ε∉⟦e₁⟧ (∣w∣≡0+w∈A⇒ε∈A {A = ⟦ e₁ ⟧ γ} ∣w₁∣≡0 w₁∈⟦e₁⟧))
   where
diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda
index 13e5ab1..fe153b1 100644
--- a/src/Cfe/Language/Properties.agda
+++ b/src/Cfe/Language/Properties.agda
@@ -850,6 +850,12 @@ Fⁿ⊆⋃F = FⁿA⊆SupFA
 ⋃-inverseʳ : ∀ (A : Language a) → ⋃ (const A) ≈ A
 ⋃-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)
+  }
+
 ------------------------------------------------------------------------
 -- Other properties of Null
 ------------------------------------------------------------------------