diff --git a/src/Examples.agda b/src/Examples.agda
index 0a7a63e1..62e0c835 100644
--- a/src/Examples.agda
+++ b/src/Examples.agda
@@ -16,5 +16,8 @@ import Examples.Exp2
 -- Amortized Analysis via Coinduction
 import Examples.Amortized
 
+-- Sequence
+import Examples.Sequence
+
 -- Effectful
 import Examples.Decalf
diff --git a/src/Examples/Sequence.agda b/src/Examples/Sequence.agda
new file mode 100644
index 00000000..43c09024
--- /dev/null
+++ b/src/Examples/Sequence.agda
@@ -0,0 +1,219 @@
+{-# OPTIONS --prop --rewriting #-}
+
+module Examples.Sequence where
+
+open import Algebra.Cost
+
+parCostMonoid = ℕ²-ParCostMonoid
+open ParCostMonoid parCostMonoid
+
+open import Calf costMonoid
+open import Calf.Parallel parCostMonoid
+
+open import Calf.Data.Product
+open import Calf.Data.Sum
+open import Calf.Data.Bool
+open import Calf.Data.Maybe
+open import Calf.Data.Nat hiding (compare)
+open import Calf.Data.List hiding (filter)
+
+open import Level using (0ℓ)
+open import Relation.Binary
+open import Data.Nat as Nat using (_<_; _+_)
+import Data.Nat.Properties as Nat
+open import Data.String using (String)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+
+open import Function using (case_of_; _$_)
+
+open import Examples.Sequence.MSequence
+open import Examples.Sequence.ListMSequence
+open import Examples.Sequence.RedBlackMSequence
+
+
+module Ex/FromList where
+  open MSequence RedBlackMSequence
+
+  fromList : cmp (Π (list nat) λ _ → F (seq nat))
+  fromList [] = empty
+  fromList (x ∷ l) =
+    bind (F (seq nat)) empty λ s₁ →
+    bind (F (seq nat)) (fromList l) λ s₂ →
+    join s₁ x s₂
+
+  example : cmp (F (seq nat))
+  example = fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
+
+
+module BinarySearchTree
+  (MSeq : MSequence)
+  (Key : StrictTotalOrder 0ℓ 0ℓ 0ℓ)
+  where
+
+  open StrictTotalOrder Key
+
+  𝕂 : tp⁺
+  𝕂 = meta⁺ (StrictTotalOrder.Carrier Key)
+
+  open MSequence MSeq public
+
+  singleton : cmp (Π 𝕂 λ _ → F (seq 𝕂))
+  singleton a =
+    bind (F (seq 𝕂)) empty λ t →
+    join t a t
+
+  Split : tp⁻
+  Split = F ((seq 𝕂) ×⁺ ((maybe 𝕂) ×⁺ (seq 𝕂)))
+
+  split : cmp (Π (seq 𝕂) λ _ → Π 𝕂 λ _ → Split)
+  split t a =
+    rec
+      {X = Split}
+      (bind Split empty λ t →
+        ret (t , nothing , t))
+      (λ t₁ ih₁ a' t₂ ih₂ →
+        case compare a a' of λ
+          { (tri< a<a' ¬a≡a' ¬a>a') →
+              bind Split ih₁ λ ( t₁₁ , a? , t₁₂ ) →
+              bind Split (join t₁₂ a' t₂) λ t →
+              ret (t₁₁ , a? , t)
+          ; (tri≈ ¬a<a' a≡a' ¬a>a') → ret (t₁ , just a' , t₂)
+          ; (tri> ¬a<a' ¬a≡a' a>a') →
+              bind Split ih₂ λ ( t₂₁ , a? , t₂₂ ) →
+              bind Split (join t₁ a' t₂₁) λ t →
+              ret (t , a? , t₂₂)
+          })
+      t
+
+  find : cmp (Π (seq 𝕂) λ _ → Π 𝕂 λ _ → F (maybe 𝕂))
+  find t a = bind (F (maybe 𝕂)) (split t a) λ { (_ , a? , _) → ret a? }
+
+  insert : cmp (Π (seq 𝕂) λ _ → Π 𝕂 λ _ → F (seq 𝕂))
+  insert t a = bind (F (seq 𝕂)) (split t a) λ { (t₁ , _ , t₂) → join t₁ a t₂ }
+
+  append : cmp (Π (seq 𝕂) λ _ → Π (seq 𝕂) λ _ → F (seq 𝕂))
+  append t₁ t₂ =
+    rec
+      {X = F (seq 𝕂)}
+      (ret t₂)
+      (λ t'₁ ih₁ a' t'₂ ih₂ →
+        bind (F (seq 𝕂)) ih₂ λ t' →
+        join t'₁ a' t')
+    t₁
+
+  delete : cmp (Π (seq 𝕂) λ _ → Π 𝕂 λ _ → F (seq 𝕂))
+  delete t a = bind (F (seq 𝕂)) (split t a) λ { (t₁ , _ , t₂) → append t₁ t₂ }
+
+  union : cmp (Π (seq 𝕂) λ _ → Π (seq 𝕂) λ _ → F (seq 𝕂))
+  union =
+    rec
+      {X = Π (seq 𝕂) λ _ → F (seq 𝕂)}
+      ret
+      λ t'₁ ih₁ a' t'₂ ih₂ t₂ →
+        bind (F (seq 𝕂)) (split t₂ a') λ { (t₂₁ , a? , t₂₂) →
+        bind (F (seq 𝕂)) ((ih₁ t₂₁) ∥ (ih₂ t₂₂)) λ (s₁ , s₂) →
+        join s₁ a' s₂ }
+
+  intersection : cmp (Π (seq 𝕂) λ _ → Π (seq 𝕂) λ _ → F (seq 𝕂))
+  intersection =
+    rec
+      {X = Π (seq 𝕂) λ _ → F (seq 𝕂)}
+      (λ t₂ → empty)
+      λ t'₁ ih₁ a' t'₂ ih₂ t₂ →
+        bind (F (seq 𝕂)) (split t₂ a') λ { (t₂₁ , a? , t₂₂) →
+        bind (F (seq 𝕂)) ((ih₁ t₂₁) ∥ (ih₂ t₂₂)) λ (s₁ , s₂) →
+          case a? of
+            λ { (just a) → join s₁ a s₂
+              ; nothing → append s₁ s₂ }
+        }
+
+  difference : cmp (Π (seq 𝕂) λ _ → Π (seq 𝕂) λ _ → F (seq 𝕂))
+  difference t₁ t₂ = helper t₁
+    where
+      helper : cmp (Π (seq 𝕂) λ _ → F (seq 𝕂))
+      helper =
+        rec
+          {X = Π (seq 𝕂) λ _ → F (seq 𝕂)}
+          ret
+          (λ t'₁ ih₁ a' t'₂ ih₂ t₁ →
+            bind (F (seq 𝕂)) (split t₁ a') λ { (t₁₁ , a? , t₁₂) →
+            bind (F (seq 𝕂)) ((ih₁ t₁₁) ∥ (ih₂ t₁₂)) λ (s₁ , s₂) →
+            append s₁ s₂
+            })
+        t₂
+
+  filter : cmp (Π (seq 𝕂) λ _ → Π (U (Π 𝕂 λ _ → F bool)) λ _ → F (seq 𝕂))
+  filter t f =
+    rec
+      {X = F (seq 𝕂)}
+      (bind (F (seq 𝕂)) empty ret)
+      (λ t'₁ ih₁ a' t'₂ ih₂ →
+        bind (F (seq 𝕂)) (ih₁ ∥ ih₂) (λ (s₁ , s₂) →
+        bind (F (seq 𝕂)) (f a') λ b →
+          if b then (join s₁ a' s₂) else (append s₁ s₂)))
+    t
+
+  mapreduce : {X : tp⁻} →
+    cmp (
+      Π (seq 𝕂) λ _ →
+      Π (U (Π 𝕂 λ _ → X)) λ _ →
+      Π (U (Π (U X) λ _ → Π (U X) λ _ → X)) λ _ →
+      Π (U X) λ _ →
+      X
+    )
+  mapreduce {X} t g f l =
+    rec {X = X} l (λ t'₁ ih₁ a' t'₂ ih₂ → f ih₁ (f (g a') ih₂)) t
+
+
+module Ex/NatSet where
+  open BinarySearchTree RedBlackMSequence Nat.<-strictTotalOrder
+
+  example : cmp Split
+  example =
+    bind Split (singleton 1) λ t₁ →
+    bind Split (insert t₁ 2) λ t₁ →
+    bind Split (singleton 4) λ t₂ →
+    bind Split (join t₁ 3 t₂) λ t →
+    split t 2
+
+  sum/seq : cmp (Π (seq nat) λ _ → F (nat))
+  sum/seq =
+    rec
+      {X = F (nat)}
+      (ret 0)
+      λ t'₁ ih₁ a' t'₂ ih₂ →
+        step (F nat) (1 , 1) $
+        bind (F (nat)) (ih₁ ∥ ih₂)
+        (λ (s₁ , s₂) → ret (s₁ + a' + s₂))
+
+
+
+module Ex/NatStringDict where
+  strictTotalOrder : StrictTotalOrder 0ℓ 0ℓ 0ℓ
+  strictTotalOrder =
+    record
+      { Carrier = ℕ × String
+      ; _≈_ = λ (n₁ , _) (n₂ , _) → n₁ ≡ n₂
+      ; _<_ = λ (n₁ , _) (n₂ , _) → n₁ Nat.< n₂
+      ; isStrictTotalOrder =
+          record
+            { isEquivalence =
+                record
+                  { refl = Eq.refl
+                  ; sym = Eq.sym
+                  ; trans = Eq.trans
+                  }
+            ; trans = Nat.<-trans
+            ; compare = λ (n₁ , _) (n₂ , _) → Nat.<-cmp n₁ n₂
+            }
+      }
+
+  open BinarySearchTree RedBlackMSequence strictTotalOrder
+
+  example : cmp Split
+  example =
+    bind Split (singleton (1 , "red")) λ t₁ →
+    bind Split (insert t₁ (2 , "orange")) λ t₁ →
+    bind Split (singleton (4 , "green")) λ t₂ →
+    bind Split (join t₁ (3 , "yellow") t₂) λ t →
+    split t (2 , "")
diff --git a/src/Examples/Sequence/DerivedFormsRBT.agda b/src/Examples/Sequence/DerivedFormsRBT.agda
new file mode 100644
index 00000000..ff1197a2
--- /dev/null
+++ b/src/Examples/Sequence/DerivedFormsRBT.agda
@@ -0,0 +1,515 @@
+{-# OPTIONS --prop --rewriting #-}
+
+module Examples.Sequence.DerivedFormsRBT where
+
+open import Algebra.Cost
+
+parCostMonoid = ℕ²-ParCostMonoid
+open ParCostMonoid parCostMonoid
+
+open import Calf costMonoid
+open import Calf.Parallel parCostMonoid
+
+open import Calf.Data.Nat
+open import Calf.Data.List
+open import Calf.Data.Product
+open import Calf.Data.IsBounded costMonoid
+open import Calf.Data.IsBoundedG costMonoid
+open import Data.List as List hiding (sum; map)
+import Data.List.Properties as List
+open import Data.Nat as Nat using (_+_; _*_)
+import Data.Nat.Properties as Nat
+open import Data.Nat.Logarithm
+
+open import Function using (_$_)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning)
+
+open import Examples.Sequence.RedBlackTree
+
+module _ {A : Set} where
+  list/preserves/length : ∀ (l₁ : List A) a (l₂ : List A) → 1 + (length l₁ + length l₂) ≡ length (l₁ ++ a ∷ l₂)
+  list/preserves/length l₁ a l₂ =
+    let open ≡-Reasoning in
+    begin
+      1 + (length l₁ + length l₂)
+    ≡˘⟨ Nat.+-assoc 1 (length l₁) (length l₂) ⟩
+      1 + length l₁ + length l₂
+    ≡⟨ Eq.cong₂ _+_ (Nat.+-comm 1 (length l₁)) refl ⟩
+      length l₁ + 1 + length l₂
+    ≡⟨ Nat.+-assoc (length l₁) 1 (length l₂) ⟩
+      length l₁ + (1 + length l₂)
+    ≡⟨⟩
+      length l₁ + length (a ∷ l₂)
+    ≡˘⟨ List.length-++ l₁ ⟩
+      length (l₁ ++ a ∷ l₂)
+    ∎
+
+  list/preserves/length' : ∀ (l₁ : List A) a (l₂ : List A) → (length l₁ + length l₂) + 1 ≡ length (l₁ ++ a ∷ l₂)
+  list/preserves/length' l₁ a l₂ =
+    let open ≡-Reasoning in
+    begin
+      (length l₁ + length l₂) + 1
+    ≡⟨ Nat.+-comm (length l₁ + length l₂) 1 ⟩
+      1 + (length l₁ + length l₂)
+    ≡⟨ list/preserves/length l₁ a l₂ ⟩
+      length (l₁ ++ a ∷ l₂)
+    ∎
+
+
+module MapReduce {A B : tp⁺} where
+  mapreduce/seq : cmp $
+    Π color λ y → Π nat λ n → Π (list A) λ l → Π (irbt A y n l) λ _ →
+    Π (U (Π A λ _ → F B)) λ _ →
+    Π (U (Π B λ _ → Π B λ _ → F B)) λ _ →
+    Π B λ _ →
+    F B
+  mapreduce/seq .black .zero .[] leaf f g z = ret z
+  mapreduce/seq .red n l (red t₁ a t₂) f g z =
+    bind (F B)
+      ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ s →
+        bind (F B) (f a) (λ b →
+          bind (F B) (g b (proj₂ s)) (λ s₃ →
+            bind (F B) (g (proj₁ s) s₃) ret))
+  mapreduce/seq .black n@(suc n') l (black t₁ a t₂) f g z =
+    bind (F B)
+      ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ s →
+        bind (F B) (f a) (λ b →
+          bind (F B) (g b (proj₂ s)) (λ s₃ →
+            bind (F B) (g (proj₁ s) s₃) ret))
+
+  mapreduce/work : val nat → val nat → val (list A) → val nat
+  mapreduce/work c₁ c₂ l = (c₁ + 2 * c₂) * length l
+
+  mapreduce/span : val nat → val nat → val color → val nat → val nat
+  mapreduce/span c₁ c₂ red n = (2 * c₁ + 4 * c₂) * n + (c₁ + 2 * c₂)
+  mapreduce/span c₁ c₂ black n = (2 * c₁ + 4 * c₂) * n
+
+  mapreduce/span' : val nat → val nat → val nat → val nat
+  mapreduce/span' c₁ c₂ n = (2 * c₁ + 4 * c₂) * n + (c₁ + 2 * c₂)
+
+  span/bounded : (c₁ c₂ : val nat) → (y : val color) → (n : val nat) → mapreduce/span c₁ c₂ y n Nat.≤ mapreduce/span' c₁ c₂ n
+  span/bounded c₁ c₂ red n = Nat.≤-refl
+  span/bounded c₁ c₂ black n = Nat.m≤m+n ((2 * c₁ + 4 * c₂) * n) (c₁ + 2 * c₂)
+
+  mapreduce/is-bounded' :
+    {c₁ c₁' c₂ c₂' : val nat} →
+    (f : cmp (Π A λ _ → F B)) →
+    ({x : val A} → IsBounded B (f x) (c₁ , c₁')) →
+    (g : cmp (Π B λ _ → Π B λ _ → F B)) →
+    ({x y : val B} → IsBounded B (g x y) (c₂ , c₂')) →
+    (z : val B) →
+    (y : val color) → (n : val nat) → (l : val (list A)) → (t : val (irbt A y n l)) →
+    IsBounded B (mapreduce/seq y n l t f g z) (mapreduce/work c₁ c₂ l , mapreduce/span c₁' c₂' y n)
+  mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z .black .zero .[] leaf =
+    Eq.subst₂
+      (λ c c' → IsBounded B (mapreduce/seq black 0 [] leaf f g z) (c , c'))
+      (Eq.sym (Nat.*-zeroʳ (c₁ + 2 * c₂)))
+      (Eq.sym (Nat.*-zeroʳ (2 * c₁' + 4 * c₂')))
+      ≤⁻-refl
+  mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z .red n l (red {l₁ = l₁} {l₂ = l₂} t₁ a t₂) =
+    let open ≤⁻-Reasoning cost in
+      begin
+        bind cost (
+          bind (F B)
+            ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ _ →
+              bind (F B) (f a) (λ _ →
+                bind (F B) (g _ _) (λ _ →
+                  bind (F B) (g _ _) ret)))
+          (λ _ → ret triv)
+      ≡⟨⟩
+        (
+          bind cost
+            ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) →
+              bind cost (f a) λ b →
+                bind cost (g b s₂) λ s₃ →
+                  bind cost (g s₁ s₃) λ _ →
+                    ret triv
+        )
+      ≤⟨ bind-monoʳ-≤⁻ ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) (λ (s₁ , s₂) →
+           bind-monoʳ-≤⁻ (f a) (λ b →
+             bind-monoʳ-≤⁻ (g b s₂) (λ s₃ → g-bound))) ⟩
+       (
+          bind cost
+            ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) →
+              bind cost (f a) λ b →
+                bind cost (g b s₂) λ _ →
+                  step⋆ (c₂ , c₂')
+        )
+      ≤⟨ bind-monoʳ-≤⁻ ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) (λ (s₁ , s₂) →
+           bind-monoʳ-≤⁻ (f a) (λ b →
+             bind-monoˡ-≤⁻ (λ _ → step⋆ (c₂ , c₂')) g-bound)) ⟩
+        (
+          bind cost
+            ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) →
+              bind cost (f a) λ b →
+                bind cost (step⋆ (c₂ , c₂')) λ _ →
+                  step⋆ (c₂ , c₂')
+        )
+      ≤⟨ bind-monoʳ-≤⁻ ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) (λ (s₁ , s₂) →
+          bind-monoˡ-≤⁻ (λ _ → bind cost (step⋆ (c₂ , c₂')) λ _ → step⋆ (c₂ , c₂')) f-bound) ⟩
+        (
+          bind cost
+            ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) →
+              bind cost (step⋆ (c₁ , c₁')) λ _ →
+                bind cost (step⋆ (c₂ , c₂')) λ _ →
+                  step⋆ (c₂ , c₂')
+        )
+      ≤⟨ bind-monoˡ-≤⁻ (λ _ → bind cost (step⋆ (c₁ , c₁')) λ _ → bind cost (step⋆ (c₂ , c₂')) λ _ → step⋆ (c₂ , c₂'))
+          (bound/par
+            {e₁ = mapreduce/seq _ _ _ t₁ f g z}
+            {c₁ = mapreduce/work c₁ c₂ l₁ , mapreduce/span c₁' c₂' black n}
+            (mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z black n l₁ t₁)
+            (mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z black n l₂ t₂)) ⟩
+        (
+          bind cost (step⋆ ((mapreduce/work c₁ c₂ l₁ , mapreduce/span c₁' c₂' black n) ⊗ (mapreduce/work c₁ c₂ l₂ , mapreduce/span c₁' c₂' black n))) λ _ →
+            bind cost (step⋆ (c₁ , c₁')) λ _ →
+              bind cost (step⋆ (c₂ , c₂')) λ _ →
+                step⋆ (c₂ , c₂')
+        )
+      ≡⟨ Eq.cong
+          (λ c → bind cost (step⋆ c) (λ _ →
+                  bind cost (step⋆ (c₁ , c₁')) λ _ →
+                    bind cost (step⋆ (c₂ , c₂')) λ _ →
+                      step⋆ (c₂ , c₂')))
+          {x = (mapreduce/work c₁ c₂ l₁ , mapreduce/span c₁' c₂' black n) ⊗ (mapreduce/work c₁ c₂ l₂ , mapreduce/span c₁' c₂' black n)}
+          (Eq.cong₂ _,_ refl (Nat.⊔-idem (mapreduce/span c₁' c₂' black n))) ⟩
+        (
+          bind cost (step⋆ (((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂) , (2 * c₁' + 4 * c₂') * n)) λ _ →
+            bind cost (step⋆ (c₁ , c₁')) λ _ →
+              bind cost (step⋆ (c₂ , c₂')) λ _ →
+                step⋆ (c₂ , c₂')
+        )
+      ≡⟨⟩
+        step⋆ ((((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂)) + (c₁ + (c₂ + c₂)) ,
+              ((2 * c₁' + 4 * c₂') * n) + (c₁' + (c₂' + c₂')))
+      ≡⟨ Eq.cong₂ (λ c c' → step⋆ (c , c')) arithemtic₁ arithemtic₂ ⟩
+        step⋆ (mapreduce/work c₁ c₂ l , mapreduce/span c₁' c₂' red n)
+      ∎
+        where
+          arithemtic₁ : (((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂)) + (c₁ + (c₂ + c₂)) ≡ (c₁ + 2 * c₂) * length l
+          arithemtic₁ =
+            let open ≡-Reasoning in
+            begin
+              (((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂)) + (c₁ + (c₂ + c₂))
+            ≡˘⟨ Eq.cong₂ _+_
+                (Nat.*-distribˡ-+ (c₁ + 2 * c₂) (length l₁) (length l₂))
+                (Eq.cong₂ _+_ {x = c₁} refl (Eq.trans (Nat.*-distribʳ-+ c₂ 1 1) (Eq.cong₂ _+_ (Nat.*-identityˡ c₂) (Nat.*-identityˡ c₂)))) ⟩
+              ((c₁ + 2 * c₂) * (length l₁ + length l₂)) + (c₁ + 2 * c₂)
+            ≡˘⟨ Eq.cong₂ _+_ refl (Nat.*-identityʳ (c₁ + 2 * c₂)) ⟩
+              ((c₁ + 2 * c₂) * (length l₁ + length l₂)) + (c₁ + 2 * c₂) * 1
+            ≡˘⟨ Nat.*-distribˡ-+ (c₁ + 2 * c₂) (length l₁ + length l₂) 1 ⟩
+              (c₁ + 2 * c₂) * (length l₁ + length l₂ + 1)
+            ≡⟨ Eq.cong₂ _*_ {x = c₁ + 2 * c₂} refl (list/preserves/length' l₁ a l₂) ⟩
+              (c₁ + 2 * c₂) * length l
+            ∎
+
+          arithemtic₂ : (2 * c₁' + 4 * c₂') * n + (c₁' + (c₂' + c₂')) ≡ (2 * c₁' + 4 * c₂') * n + (c₁' + 2 * c₂')
+          arithemtic₂ =
+            let open ≡-Reasoning in
+            begin
+              (2 * c₁' + 4 * c₂') * n + (c₁' + (c₂' + c₂'))
+            ≡˘⟨ Eq.cong₂ _+_
+                {x = (2 * c₁' + 4 * c₂') * n}
+                refl
+                (Eq.cong₂ _+_ {x = c₁'} refl (Eq.trans (Nat.*-distribʳ-+ c₂' 1 1) (Eq.cong₂ _+_ (Nat.*-identityˡ c₂') (Nat.*-identityˡ c₂')))) ⟩
+              (2 * c₁' + 4 * c₂') * n + (c₁' + 2 * c₂')
+            ∎
+  mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z .black n@(suc n') l (black {y₁ = y₁} {y₂ = y₂} {l₁ = l₁} {l₂ = l₂} t₁ a t₂) =
+    let open ≤⁻-Reasoning cost in
+      begin
+        bind cost (
+          bind (F B)
+            ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ _ →
+              bind (F B) (f a) (λ _ →
+                bind (F B) (g _ _) (λ _ →
+                  bind (F B) (g _ _) ret)))
+          (λ _ → ret triv)
+      ≡⟨⟩
+        (
+          bind cost
+            ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) →
+              bind cost (f a) λ b →
+                bind cost (g b s₂) λ s₃ →
+                  bind cost (g s₁ s₃) λ _ →
+                    ret triv
+        )
+      ≤⟨ bind-monoʳ-≤⁻ ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) (λ (s₁ , s₂) →
+           bind-monoʳ-≤⁻ (f a) (λ b →
+             bind-monoʳ-≤⁻ (g b s₂) (λ s₃ → g-bound))) ⟩
+       (
+          bind cost
+            ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) →
+              bind cost (f a) λ b →
+                bind cost (g b s₂) λ _ →
+                  step⋆ (c₂ , c₂')
+        )
+      ≤⟨ bind-monoʳ-≤⁻ ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) (λ (s₁ , s₂) →
+           bind-monoʳ-≤⁻ (f a) (λ b →
+             bind-monoˡ-≤⁻ (λ _ → step⋆ (c₂ , c₂')) g-bound)) ⟩
+        (
+          bind cost
+            ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) →
+              bind cost (f a) λ b →
+                bind cost (step⋆ (c₂ , c₂')) λ _ →
+                  step⋆ (c₂ , c₂')
+        )
+      ≤⟨ bind-monoʳ-≤⁻ ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) (λ (s₁ , s₂) →
+          bind-monoˡ-≤⁻ (λ _ → bind cost (step⋆ (c₂ , c₂')) λ _ → step⋆ (c₂ , c₂')) f-bound) ⟩
+        (
+          bind cost
+            ((mapreduce/seq _ _ _ t₁ f g z) ∥ (mapreduce/seq _ _ _ t₂ f g z)) λ (s₁ , s₂) →
+              bind cost (step⋆ (c₁ , c₁')) λ _ →
+                bind cost (step⋆ (c₂ , c₂')) λ _ →
+                  step⋆ (c₂ , c₂')
+        )
+      ≤⟨ bind-monoˡ-≤⁻ (λ _ → bind cost (step⋆ (c₁ , c₁')) λ _ → bind cost (step⋆ (c₂ , c₂')) λ _ → step⋆ (c₂ , c₂'))
+          (bound/par
+            {e₁ = mapreduce/seq _ _ _ t₁ f g z}
+            {c₁ = mapreduce/work c₁ c₂ l₁ , mapreduce/span c₁' c₂' y₁ n'}
+            (mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z y₁ n' l₁ t₁)
+            (mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z y₂ n' l₂ t₂)) ⟩
+        (
+          bind cost (step⋆ ((mapreduce/work c₁ c₂ l₁ , mapreduce/span c₁' c₂' y₁ n') ⊗ (mapreduce/work c₁ c₂ l₂ , mapreduce/span c₁' c₂' y₂ n'))) λ _ →
+            bind cost (step⋆ (c₁ , c₁')) λ _ →
+              bind cost (step⋆ (c₂ , c₂')) λ _ →
+                step⋆ (c₂ , c₂')
+        )
+      ≤⟨ bind-monoˡ-≤⁻
+          (λ _ →
+            bind cost (step⋆ (c₁ , c₁')) λ _ →
+              bind cost (step⋆ (c₂ , c₂')) λ _ →
+                step⋆ (c₂ , c₂'))
+          (step⋆-mono-≤⁻ {c = mapreduce/work c₁ c₂ l₁ + mapreduce/work c₁ c₂ l₂ , mapreduce/span c₁' c₂' y₁ n' Nat.⊔ mapreduce/span c₁' c₂' y₂ n'}
+            (Nat.≤-refl , Nat.⊔-mono-≤ (span/bounded c₁' c₂' y₁ n') (span/bounded c₁' c₂' y₂ n'))) ⟩
+        (
+          bind cost (step⋆ ((mapreduce/work c₁ c₂ l₁ , mapreduce/span' c₁' c₂' n') ⊗ (mapreduce/work c₁ c₂ l₂ , mapreduce/span' c₁' c₂' n'))) λ _ →
+            bind cost (step⋆ (c₁ , c₁')) λ _ →
+              bind cost (step⋆ (c₂ , c₂')) λ _ →
+                step⋆ (c₂ , c₂')
+        )
+      ≡⟨ Eq.cong
+          (λ c → bind cost (step⋆ c) λ _ →
+            bind cost (step⋆ (c₁ , c₁')) λ _ →
+              bind cost (step⋆ (c₂ , c₂')) λ _ →
+                step⋆ (c₂ , c₂'))
+          {x = mapreduce/work c₁ c₂ l₁ + mapreduce/work c₁ c₂ l₂ , mapreduce/span' c₁' c₂' n' Nat.⊔ mapreduce/span' c₁' c₂' n'}
+          (Eq.cong₂ _,_ refl (Nat.⊔-idem ((2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂')))) ⟩
+        (
+          bind cost (step⋆ (((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂) , (2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂'))) λ _ →
+            bind cost (step⋆ (c₁ , c₁')) λ _ →
+              bind cost (step⋆ (c₂ , c₂')) λ _ →
+                step⋆ (c₂ , c₂')
+        )
+      ≡⟨⟩
+        step⋆ (((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂) + (c₁ + (c₂ + c₂)) ,
+               ((2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂')) + (c₁' + (c₂' + c₂')) )
+      ≡⟨ Eq.cong₂ (λ c c' → step⋆ (c , c')) arithemtic₁ arithemtic₂ ⟩
+        step⋆ (mapreduce/work c₁ c₂ l , mapreduce/span c₁' c₂' black n)
+      ∎
+        where
+          arithemtic₁ : ((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂) + (c₁ + (c₂ + c₂)) ≡ (c₁ + 2 * c₂) * length l
+          arithemtic₁ =
+            let open ≡-Reasoning in
+            begin
+              (((c₁ + 2 * c₂) * length l₁) + ((c₁ + 2 * c₂) * length l₂)) + (c₁ + (c₂ + c₂))
+            ≡˘⟨ Eq.cong₂ _+_
+                (Nat.*-distribˡ-+ (c₁ + 2 * c₂) (length l₁) (length l₂))
+                (Eq.cong₂ _+_ {x = c₁} refl (Eq.trans (Nat.*-distribʳ-+ c₂ 1 1) (Eq.cong₂ _+_ (Nat.*-identityˡ c₂) (Nat.*-identityˡ c₂)))) ⟩
+              ((c₁ + 2 * c₂) * (length l₁ + length l₂)) + (c₁ + 2 * c₂)
+            ≡˘⟨ Eq.cong₂ _+_ refl (Nat.*-identityʳ (c₁ + 2 * c₂)) ⟩
+              ((c₁ + 2 * c₂) * (length l₁ + length l₂)) + (c₁ + 2 * c₂) * 1
+            ≡˘⟨ Nat.*-distribˡ-+ (c₁ + 2 * c₂) (length l₁ + length l₂) 1 ⟩
+              (c₁ + 2 * c₂) * (length l₁ + length l₂ + 1)
+            ≡⟨ Eq.cong₂ _*_ {x = c₁ + 2 * c₂} refl (list/preserves/length' l₁ a l₂) ⟩
+              (c₁ + 2 * c₂) * length l
+            ∎
+
+          arithemtic₂ : ((2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂')) + (c₁' + (c₂' + c₂')) ≡ (2 * c₁' + 4 * c₂') * n
+          arithemtic₂ =
+            let open ≡-Reasoning in
+            begin
+              ((2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂')) + (c₁' + (c₂' + c₂'))
+            ≡˘⟨ Eq.cong₂ _+_
+                {x = (2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂')}
+                refl
+                (Eq.cong₂ _+_ {x = c₁'} refl (Eq.trans (Nat.*-distribʳ-+ c₂' 1 1) (Eq.cong₂ _+_ (Nat.*-identityˡ c₂') (Nat.*-identityˡ c₂')))) ⟩
+              ((2 * c₁' + 4 * c₂') * n' + (c₁' + 2 * c₂')) + (c₁' + 2 * c₂')
+            ≡⟨ Nat.+-assoc ((2 * c₁' + 4 * c₂') * n') (c₁' + 2 * c₂') (c₁' + 2 * c₂') ⟩
+              (2 * c₁' + 4 * c₂') * n' + ((c₁' + 2 * c₂') + (c₁' + 2 * c₂'))
+            ≡˘⟨ Eq.cong₂ _+_
+                {x = (2 * c₁' + 4 * c₂') * n'}
+                refl
+                (Eq.trans (Nat.*-distribʳ-+ (c₁' + 2 * c₂') 1 1) (Eq.cong₂ _+_ (Nat.*-identityˡ (c₁' + 2 * c₂')) (Nat.*-identityˡ (c₁' + 2 * c₂')))) ⟩
+              (2 * c₁' + 4 * c₂') * n' + 2 * (c₁' + 2 * c₂')
+            ≡⟨ Eq.cong₂ _+_
+                {x = (2 * c₁' + 4 * c₂') * n'}
+                refl
+                (Nat.*-distribˡ-+ 2 c₁' (2 * c₂')) ⟩
+              (2 * c₁' + 4 * c₂') * n' + (2 * c₁' + 2 * (2 * c₂'))
+            ≡⟨ Eq.cong (λ x → (2 * c₁' + 4 * c₂') * n' + (2 * c₁' + x)) (Eq.sym (Nat.*-assoc 2 2 c₂')) ⟩
+              (2 * c₁' + 4 * c₂') * n' + (2 * c₁' + 4 * c₂')
+            ≡⟨ Nat.+-comm ((2 * c₁' + 4 * c₂') * n') (2 * c₁' + 4 * c₂') ⟩
+              (2 * c₁' + 4 * c₂') + (2 * c₁' + 4 * c₂') * n'
+            ≡˘⟨ Nat.*-suc (2 * c₁' + 4 * c₂') n' ⟩
+              (2 * c₁' + 4 * c₂') * n
+            ∎
+
+  mapreduce/is-bounded :
+    {c₁ c₁' c₂ c₂' : val nat} →
+    (f : cmp (Π A λ _ → F B)) →
+    ({x : val A} → IsBounded B (f x) (c₁ , c₁')) →
+    (g : cmp (Π B λ _ → Π B λ _ → F B)) →
+    ({x y : val B} → IsBounded B (g x y) (c₂ , c₂')) →
+    (z : val B) →
+    (y : val color) → (n : val nat) → (l : val (list A)) → (t : val (irbt A y n l)) →
+    IsBounded B (mapreduce/seq y n l t f g z) ((c₁ + 2 * c₂) * length l , (2 * c₁' + 4 * c₂') * ⌈log₂ (1 + length l) ⌉ + (c₁' + 2 * c₂'))
+  mapreduce/is-bounded {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z y n l t =
+    let open ≤⁻-Reasoning cost in
+      begin
+        bind cost (mapreduce/seq y n l t f g z) (λ _ → ret triv)
+      ≤⟨ mapreduce/is-bounded' {c₁} {c₁'} {c₂} {c₂'} f f-bound g g-bound z y n l t ⟩
+        step⋆ (mapreduce/work c₁ c₂ l , mapreduce/span c₁' c₂' y n)
+      ≤⟨ step⋆-mono-≤⁻ (Nat.≤-refl {mapreduce/work c₁ c₂ l}, span/bounded c₁' c₂' y n) ⟩
+        step⋆ (mapreduce/work c₁ c₂ l , mapreduce/span' c₁' c₂' n)
+      ≤⟨ step⋆-mono-≤⁻ (Nat.≤-refl {mapreduce/work c₁ c₂ l} , lemma) ⟩
+        step⋆ ((c₁ + 2 * c₂) * length l , (2 * c₁' + 4 * c₂') * ⌈log₂ (1 + length l) ⌉ + (c₁' + 2 * c₂'))
+      ∎
+        where
+          lemma : mapreduce/span' c₁' c₂' n Nat.≤ (2 * c₁' + 4 * c₂') * ⌈log₂ (1 + length l) ⌉ + (c₁' + 2 * c₂')
+          lemma =
+            let open Nat.≤-Reasoning in
+              begin
+                (2 * c₁' + 4 * c₂') * n + (c₁' + 2 * c₂')
+              ≤⟨ Nat.+-monoˡ-≤ (c₁' + 2 * c₂') (Nat.*-monoʳ-≤ (2 * c₁' + 4 * c₂') (i-nodes/bound/log-node-black-height t)) ⟩
+                (2 * c₁' + 4 * c₂') * ⌈log₂ (1 + i-nodes t) ⌉ + (c₁' + 2 * c₂')
+              ≡⟨ Eq.cong (λ x → (2 * c₁' + 4 * c₂') * ⌈log₂ (1 + x) ⌉ + (c₁' + 2 * c₂')) (i-nodes≡lengthl t) ⟩
+                (2 * c₁' + 4 * c₂') * ⌈log₂ (1 + length l) ⌉ + (c₁' + 2 * c₂')
+              ∎
+
+
+module Sum where
+  sum/seq : cmp $
+    Π color λ y → Π nat λ n → Π (list nat) λ l → Π (irbt nat y n l) λ _ → F nat
+  sum/seq .black .zero .[] leaf = ret 0
+  sum/seq .red n l (red t₁ a t₂) =
+    step (F nat) (1 , 1) $
+      bind (F (nat)) ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂))
+      (λ (s₁ , s₂) → ret (s₁ + a + s₂))
+  sum/seq .black n l (black t₁ a t₂) =
+    step (F nat) (1 , 1) $
+      bind (F (nat)) ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂))
+      (λ (s₁ , s₂) → ret (s₁ + a + s₂))
+
+  span/sum : val color → val nat → val nat
+  span/sum red n = 1 + 2 * n
+  span/sum black n = 2 * n
+
+  span/bounded : ∀ y n → (span/sum y n) Nat.≤ (1 + 2 * n)
+  span/bounded red n = Nat.≤-refl
+  span/bounded black n = Nat.n≤1+n (2 * n)
+
+  sum/bounded' : ∀ y n l t → IsBounded nat (sum/seq y n l t) (length l , span/sum y n)
+  sum/bounded' .black .zero .[] leaf = ≤⁻-refl
+  sum/bounded' .red n l (red {l₁ = l₁} {l₂ = l₂} t₁ a t₂) =
+    let open ≤⁻-Reasoning cost in
+      begin
+        step cost (1 , 1) (
+          bind cost (
+            bind (F (nat)) ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂))
+              (λ (s₁ , s₂) → ret (s₁ + a + s₂)))
+          (λ _ → ret triv))
+      ≡⟨⟩
+        step cost (1 , 1) (
+          bind cost ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂))
+            (λ _ → ret triv))
+      ≤⟨
+        ≤⁻-mono
+          (step cost (1 , 1))
+          (bound/par
+            {e₁ = sum/seq _ _ _ t₁}
+            {c₁ = (length l₁ , span/sum black n)}
+            (sum/bounded' black n l₁ t₁)
+            (sum/bounded' black n l₂ t₂))
+      ⟩
+        step cost (1 , 1) (
+          step⋆ ((length l₁ , span/sum black n) ⊗ (length l₂ , span/sum black n)))
+      ≡⟨ Eq.cong (λ c → step cost (1 , 1) (step⋆ c)) (Eq.cong₂ _,_ refl (Nat.⊔-idem (span/sum black n))) ⟩
+        step cost (1 , 1) (
+          step⋆ (length l₁ + length l₂ , span/sum black n))
+      ≡⟨⟩
+        step⋆ (1 + (length l₁ + length l₂) , 1 + 2 * n)
+      ≡⟨ Eq.cong₂ (λ c₁ c₂ → step⋆ (c₁ , c₂)) (list/preserves/length l₁ a l₂) refl ⟩
+        step⋆ (length l , span/sum red n)
+      ∎
+  sum/bounded' .black n@(suc n') l (black {y₁ = y₁} {y₂ = y₂} {l₁ = l₁} {l₂ = l₂} t₁ a t₂) =
+    let open ≤⁻-Reasoning cost in
+      begin
+        step cost (1 , 1) (
+          bind cost (
+            bind (F (nat)) ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂))
+              (λ (s₁ , s₂) → ret (s₁ + a + s₂)))
+          (λ _ → ret triv))
+      ≡⟨⟩
+        step cost (1 , 1) (
+          bind cost ((sum/seq _ _ _ t₁) ∥ (sum/seq _ _ _ t₂))
+            (λ _ → ret triv))
+      ≤⟨ ≤⁻-mono
+          (step cost (1 , 1))
+          (bound/par
+            {e₁ = sum/seq _ _ _ t₁}
+            {c₁ = (length l₁ , span/sum y₁ n')}
+            (sum/bounded' y₁ n' l₁ t₁)
+            (sum/bounded' y₂ n' l₂ t₂)) ⟩
+        step cost (1 , 1) (
+          step⋆ ((length l₁ , span/sum y₁ n') ⊗ (length l₂ , span/sum y₂ n')))
+      ≤⟨ ≤⁻-mono
+          (λ e → step cost (1 , 1) e)
+            (step⋆-mono-≤⁻
+              (Nat.≤-refl , Nat.⊔-mono-≤ (span/bounded y₁ n') (span/bounded y₂ n'))) ⟩
+        step cost (1 , 1) (
+          step⋆ ((length l₁ , 1 + 2 * n') ⊗ (length l₂ , 1 + 2 * n')))
+      ≡⟨ Eq.cong (λ c → step cost (1 , 1) (step⋆ c)) (Eq.cong₂ _,_ refl (Nat.⊔-idem (1 + 2 * n'))) ⟩
+        step cost (1 , 1) (
+          step⋆ (length l₁ + length l₂ , 1 + 2 * n'))
+      ≡⟨⟩
+        step⋆ (1 + (length l₁ + length l₂) , 1 + (1 + 2 * n'))
+      ≡⟨ Eq.cong₂ (λ c₁ c₂ → step⋆ (c₁ , c₂)) (list/preserves/length l₁ a l₂) (arithemtic n') ⟩
+       step⋆ (length l , span/sum black n)
+      ∎
+        where
+          arithemtic : ∀ n → 1 + (1 + 2 * n) ≡ 2 * (suc n)
+          arithemtic n =
+            let open ≡-Reasoning in
+            begin
+              1 + (1 + 2 * n)
+            ≡⟨ Nat.+-assoc 1 1 (2 * n) ⟩
+              (1 + 1) + 2 * n
+            ≡⟨⟩
+              2 + 2 * n
+            ≡˘⟨ Nat.*-suc 2 n ⟩
+              2 * (suc n)
+            ∎
+
+  sum/bounded : ∀ y n l t → IsBounded nat (sum/seq y n l t) (length l , 1 + 2 * ⌈log₂ (1 + length l) ⌉)
+  sum/bounded y n l t =
+    let open ≤⁻-Reasoning cost in
+      begin
+        bind cost (sum/seq y n l t) (λ _ → ret triv)
+      ≤⟨ sum/bounded' y n l t ⟩
+        step⋆ (length l , span/sum y n)
+      ≤⟨ step⋆-mono-≤⁻ (Nat.≤-refl {length l} , lemma) ⟩
+        step⋆ (length l , 1 + 2 * ⌈log₂ (1 + length l) ⌉)
+      ∎
+    where
+      lemma : span/sum y n Nat.≤ 1 + (2 * ⌈log₂ (1 + length l) ⌉)
+      lemma =
+        let open Nat.≤-Reasoning in
+        begin
+          span/sum y n
+        ≤⟨ span/bounded y n ⟩
+          1 + (2 * n)
+        ≤⟨ Nat.s≤s (Nat.*-monoʳ-≤ 2 (i-nodes/bound/log-node-black-height t)) ⟩
+          1 + (2 * ⌈log₂ (1 + i-nodes t) ⌉)
+        ≡⟨ Eq.cong (λ x → 1 + (2 * ⌈log₂ (1 + x) ⌉)) (i-nodes≡lengthl t) ⟩
+          1 + (2 * ⌈log₂ (1 + length l) ⌉)
+        ∎
diff --git a/src/Examples/Sequence/ListMSequence.agda b/src/Examples/Sequence/ListMSequence.agda
new file mode 100644
index 00000000..768f7f6a
--- /dev/null
+++ b/src/Examples/Sequence/ListMSequence.agda
@@ -0,0 +1,35 @@
+{-# OPTIONS --prop --rewriting #-}
+
+module Examples.Sequence.ListMSequence where
+
+open import Algebra.Cost
+
+parCostMonoid = ℕ²-ParCostMonoid
+open ParCostMonoid parCostMonoid
+
+open import Calf costMonoid
+open import Calf.Data.List
+open import Data.Nat as Nat using (_+_)
+
+open import Examples.Sequence.MSequence
+
+ListMSequence : MSequence
+ListMSequence =
+  record
+    { seq = list
+    ; empty = ret []
+    ; join =
+        λ {A} l₁ a l₂ →
+          let n = length l₁ + 1 + length l₂ in
+          step (F (list A)) (n , n) (ret (l₁ ++ [ a ] ++ l₂))
+    ; rec = λ {A} {X} → rec {A} {X}
+    }
+  where
+    rec : {X : tp⁻} →
+      cmp
+        ( Π (U X) λ _ →
+          Π (U (Π (list A) λ _ → Π (U X) λ _ → Π A λ _ → Π (list A) λ _ → Π (U X) λ _ → X)) λ _ →
+          Π (list A) λ _ → X
+        )
+    rec {A} {X} z f []      = z
+    rec {A} {X} z f (x ∷ l) = step X (1 , 1) (f [] z x l (rec {A} {X} z f l))
diff --git a/src/Examples/Sequence/MSequence.agda b/src/Examples/Sequence/MSequence.agda
new file mode 100644
index 00000000..bed07a64
--- /dev/null
+++ b/src/Examples/Sequence/MSequence.agda
@@ -0,0 +1,25 @@
+{-# OPTIONS --prop --rewriting #-}
+
+module Examples.Sequence.MSequence where
+
+open import Algebra.Cost
+
+parCostMonoid = ℕ²-ParCostMonoid
+open ParCostMonoid parCostMonoid
+
+open import Calf costMonoid
+
+-- Middle Sequence
+record MSequence : Set where
+  field
+    seq : tp⁺ → tp⁺
+
+    empty : cmp (F (seq A))
+    join : cmp (Π (seq A) λ s₁ → Π A λ a → Π (seq A) λ s₂ → F (seq A))
+
+    rec : {X : tp⁻} →
+      cmp
+        ( Π (U X) λ _ →
+          Π (U (Π (seq A) λ _ → Π (U X) λ _ → Π A λ _ → Π (seq A) λ _ → Π (U X) λ _ → X)) λ _ →
+          Π (seq A) λ _ → X
+        )
diff --git a/src/Examples/Sequence/RedBlackMSequence.agda b/src/Examples/Sequence/RedBlackMSequence.agda
new file mode 100644
index 00000000..3357fa8e
--- /dev/null
+++ b/src/Examples/Sequence/RedBlackMSequence.agda
@@ -0,0 +1,122 @@
+{-# OPTIONS --prop --rewriting #-}
+
+module Examples.Sequence.RedBlackMSequence where
+
+open import Algebra.Cost
+
+parCostMonoid = ℕ²-ParCostMonoid
+open ParCostMonoid parCostMonoid
+
+open import Calf costMonoid
+
+open import Calf.Data.Nat
+open import Calf.Data.List
+open import Calf.Data.Product
+open import Calf.Data.Sum
+open import Calf.Data.IsBounded costMonoid
+open import Calf.Data.IsBoundedG costMonoid
+
+open import Data.Nat as Nat using (_+_; _*_; ⌊_/2⌋; _≥_; _∸_)
+import Data.Nat.Properties as Nat
+open import Data.Nat.Logarithm
+
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
+
+open import Examples.Sequence.MSequence
+open import Examples.Sequence.RedBlackTree
+
+
+RedBlackMSequence : MSequence
+RedBlackMSequence =
+  record
+    { seq = rbt
+    ; empty = ret ⟪ leaf ⟫
+    ; join = join
+    ; rec = λ {A} {X} → rec {A} {X}
+    }
+  where
+    record RBT (A : tp⁺) : Set where
+      pattern
+      constructor ⟪_⟫
+      field
+        {y} : val color
+        {n} : val nat
+        {l} : val (list A)
+        t : val (irbt A y n l)
+    rbt : (A : tp⁺) → tp⁺
+    rbt A = meta⁺ (RBT A)
+
+    joinCont : ∀ (t₁ : RBT A) (t₂ : RBT A) a → Σ Color (λ c → Σ (List (val A)) (λ l → Σ (l ≡ (RBT.l t₁ ++ [ a ] ++ RBT.l t₂)) (λ x →
+        IRBT A c (suc (RBT.n t₁ ⊔ RBT.n t₂)) l ⊎ IRBT A c (RBT.n t₁ ⊔ RBT.n t₂) l))) → cmp (F (rbt A))
+    joinCont _ _ _ (_ , _ , _ , inj₁ t) = ret ⟪ t ⟫
+    joinCont _ _ _ (_ , _ , _ , inj₂ t) = ret ⟪ t ⟫
+
+    join : cmp (Π (rbt A) λ _ → Π A λ _ → Π (rbt A) λ _ → F (rbt A))
+    join {A} t₁ a t₂ = bind (F (rbt A)) (i-join _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂)) (joinCont t₁ t₂ a)
+
+    join/is-bounded : ∀ {A} t₁ a t₂ → IsBounded (rbt A) (join t₁ a t₂)
+      (1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)))
+    join/is-bounded {A} t₁ a t₂ =
+      let open ≤⁻-Reasoning cost in
+        begin
+          bind cost (
+            bind (F (rbt A)) (i-join _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂)) (joinCont t₁ t₂ a))
+          (λ _ → ret triv)
+        ≡⟨ Eq.cong
+             (λ f → bind cost (i-join _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂)) f)
+             (funext (λ { (_ , _ , _ , inj₁ _) → refl
+                        ; (_ , _ , _ , inj₂ _) → refl })) ⟩
+          bind cost (i-join _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂)) (λ _ → ret triv)
+        ≤⟨ i-join/is-bounded _ _ _ (RBT.t t₁) a _ _ _ (RBT.t t₂) ⟩
+          step⋆ (1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)))
+        ∎
+
+    nodes : RBT A → val nat
+    nodes ⟪ t ⟫ = i-nodes t
+
+    nodes/upper-bound : (t : RBT A) → RBT.n t Nat.≤ ⌈log₂ (1 + (nodes t)) ⌉
+    nodes/upper-bound ⟪ t ⟫ = i-nodes/bound/log-node-black-height t
+
+    nodes/lower-bound : (t : RBT A) → RBT.n t Nat.≥ ⌊ (⌈log₂ (1 + (nodes t)) ⌉ ∸ 1) /2⌋
+    nodes/lower-bound ⟪ t ⟫ = i-nodes/lower-bound/log-node-black-height t 
+
+    join/cost : ∀ {A} (t₁ : RBT A) (t₂ : RBT A) → ℂ
+    join/cost {A} t₁ t₂ =
+      let max = ⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ in
+      let min = ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋ in
+        (1 + 2 * (max ∸ min)) , (1 + 2 * (max ∸ min))
+
+    join/is-bounded/nodes : ∀ {A} t₁ a t₂ → IsBounded (rbt A) (join t₁ a t₂) (join/cost t₁ t₂)
+    join/is-bounded/nodes {A} t₁ a t₂ =
+      let open ≤⁻-Reasoning cost in
+        begin
+          bind cost (join t₁ a t₂) (λ _ → ret triv)
+        ≤⟨ join/is-bounded t₁ a t₂ ⟩
+          step⋆ (1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)) , 1 + (2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)))
+        ≤⟨ step⋆-mono-≤⁻ (black-height-cost/to/node-cost , black-height-cost/to/node-cost)  ⟩
+          step⋆ (join/cost t₁ t₂)
+        ∎
+          where
+            black-height-cost/to/node-cost : 1 + 2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂) Nat.≤ 1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋)
+            black-height-cost/to/node-cost =
+              let open Nat.≤-Reasoning in
+                begin
+                  1 + 2 * (RBT.n t₁ Nat.⊔ RBT.n t₂ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)
+                ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoˡ-≤ (RBT.n t₁ Nat.⊓ RBT.n t₂) (Nat.⊔-mono-≤ (nodes/upper-bound t₁) (nodes/upper-bound t₂)))) ⟩
+                  1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ RBT.n t₁ Nat.⊓ RBT.n t₂)
+                ≤⟨ Nat.+-monoʳ-≤ 1 (Nat.*-monoʳ-≤ 2 (Nat.∸-monoʳ-≤ (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉) (Nat.⊓-mono-≤ (nodes/lower-bound t₁) (nodes/lower-bound t₂)))) ⟩
+                  1 + 2 * (⌈log₂ (1 + (nodes t₁)) ⌉ Nat.⊔ ⌈log₂ (1 + (nodes t₂)) ⌉ ∸ ⌊ (⌈log₂ (1 + (nodes t₁)) ⌉ ∸ 1) /2⌋ Nat.⊓ ⌊ (⌈log₂ (1 + (nodes t₂)) ⌉ ∸ 1) /2⌋)
+                ∎
+
+    rec : {A : tp⁺} {X : tp⁻} →
+      cmp
+        ( Π (U X) λ _ →
+          Π (U (Π (rbt A) λ _ → Π (U X) λ _ → Π A λ _ → Π (rbt A) λ _ → Π (U X) λ _ → X)) λ _ →
+          Π (rbt A) λ _ → X
+        )
+    rec {A} {X} z f ⟪ t ⟫ =
+      i-rec {A} {X}
+        z
+        (λ _ _ _ t₁ ih₁ a _ _ _ t₂ ih₂ → f ⟪ t₁ ⟫ ih₁ a ⟪ t₂ ⟫ ih₂)
+        _ _ _ t
diff --git a/src/Examples/Sequence/RedBlackTree.agda b/src/Examples/Sequence/RedBlackTree.agda
new file mode 100644
index 00000000..625c915b
--- /dev/null
+++ b/src/Examples/Sequence/RedBlackTree.agda
@@ -0,0 +1,701 @@
+{-# OPTIONS --prop --rewriting #-}
+
+module Examples.Sequence.RedBlackTree where
+
+open import Algebra.Cost
+
+parCostMonoid = ℕ²-ParCostMonoid
+open ParCostMonoid parCostMonoid
+
+open import Calf costMonoid
+
+open import Calf.Data.Product
+open import Calf.Data.Sum
+open import Calf.Data.Nat
+open import Calf.Data.List
+open import Calf.Data.IsBounded costMonoid
+open import Calf.Data.IsBoundedG costMonoid
+open import Data.Nat as Nat using (_+_; _*_; _∸_)
+open import Data.Nat.Logarithm
+import Data.Nat.Properties as Nat
+import Data.List.Properties as List
+
+open import Function using (_$_)
+
+open import Relation.Nullary
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≢_; module ≡-Reasoning; ≢-sym)
+
+
+data Color : Set where
+  red : Color
+  black : Color
+color : tp⁺
+color = meta⁺ Color
+
+-- Indexed Red Black Tree
+data IRBT (A : tp⁺) : val color → val nat → val (list A) → Set where
+  leaf  : IRBT A black zero []
+  red   : {n : val nat} {l₁ l₂ : val (list A)}
+    (t₁ : IRBT A black n l₁) (a : val A) (t₂ : IRBT A black n l₂)
+    → IRBT A red n (l₁ ++ [ a ] ++ l₂)
+  black : {n : val nat} {y₁ y₂ : val color} {l₁ l₂ : val (list A)}
+    (t₁ : IRBT A y₁ n l₁) (a : val A) (t₂ : IRBT A y₂ n l₂)
+    → IRBT A black (suc n) (l₁ ++ [ a ] ++ l₂)
+irbt : (A : tp⁺) → val color → val nat → val (list A) → tp⁺
+irbt A y n l = meta⁺ (IRBT A y n l)
+
+
+data AlmostLeftRBT (A : tp⁺) : (right-color : val color) → val nat → val (list A) → Set where
+  violation :
+    {n : val nat} {l₁ l₂ : val (list A)}
+    → IRBT A red n l₁ → (a : val A) → IRBT A black n l₂
+    → AlmostLeftRBT A red n (l₁ ++ [ a ] ++ l₂)
+  valid :
+    {right-color : val color} {n : val nat} {y : val color} {l : val (list A)} → IRBT A y n l
+    → AlmostLeftRBT A right-color n l
+alrbt : (A : tp⁺) → val color → val nat → val (list A) → tp⁺
+alrbt A y n l = meta⁺ (AlmostLeftRBT A y n l)
+
+joinLeftContCase₁ : ∀ l₁ l₂₁ l₂₂ a a₁ n₂ t₂₂ →
+  (Σ (List (val A)) λ l → Σ ((l ≡ l₁ ++ [ a ] ++ l₂₁)) (λ _ → (AlmostLeftRBT A black n₂ l))) →
+    cmp (F (Σ⁺ (list A) λ l → (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂₁ ++ [ a₁ ] ++ l₂₂)) ×⁺ (alrbt A red n₂ l)))
+joinLeftContCase₁ {A} l₁ l₂₁ l₂₂ a a₁ n₂ t₂₂ (l , l≡l₂₁++a₁∷l₂₂ , valid {y = red} t') =
+  ret (((l₁ ++ [ a ] ++ l₂₁) ++ [ a₁ ] ++ l₂₂) ,
+    (List.++-assoc l₁ (a ∷ l₂₁) (a₁ ∷ l₂₂) ,
+    (Eq.subst (λ l' → AlmostLeftRBT A red n₂ l') (Eq.cong₂ _++_ l≡l₂₁++a₁∷l₂₂ refl) (violation t' a₁ t₂₂))))
+joinLeftContCase₁ {A} l₁ l₂₁ l₂₂ a a₁ n₂ t₂₂ (l , l≡l₂₁++a₁∷l₂₂ , valid {y = black} t') =
+  ret (((l₁ ++ [ a ] ++ l₂₁) ++ [ a₁ ] ++ l₂₂) ,
+    (List.++-assoc l₁ (a ∷ l₂₁) (a₁ ∷ l₂₂) ,
+    Eq.subst (λ l' → AlmostLeftRBT A red n₂ l') (Eq.cong₂ _++_ l≡l₂₁++a₁∷l₂₂ refl) (valid (red t' a₁ t₂₂))))
+
+joinLeftContCase₂ : ∀ l₁ l₂₁ l₂₂ a a₁ y₂₁ y₂₂ n₂ (t₂₂ : IRBT A y₂₂ n₂ l₂₂) →
+  (Σ (List (val A))(λ a₂ → Σ (a₂ ≡ l₁ ++ a ∷ l₂₁) (λ x → AlmostLeftRBT A y₂₁ n₂ a₂))) →
+    cmp (F (Σ⁺ (list A) (λ l → meta⁺ (l ≡ l₁ ++ a ∷ l₂₁ ++ a₁ ∷ l₂₂) ×⁺ alrbt A black (suc n₂) l)))
+joinLeftContCase₂ {A} l₁ l₂₁ l₂₂ a a₁ y₂₁ y₂₂ n₂ t₂₂ (l , l≡l₁++a∷l₂₁ , violation {l₂ = l'₂} (red {l₁ = l'₁₁} {l₂ = l'₁₂} t'₁₁ a'₁ t'₁₂) a' t'₂) =
+  ret ((l'₁₁ ++ [ a'₁ ] ++ l'₁₂) ++ [ a' ] ++ (l'₂ ++ [ a₁ ] ++ l₂₂) ,
+    ((begin
+        (l'₁₁ ++ a'₁ ∷ l'₁₂) ++ a' ∷ l'₂ ++ a₁ ∷ l₂₂
+      ≡˘⟨ List.++-assoc (l'₁₁ ++ a'₁ ∷ l'₁₂) (a' ∷ l'₂) (a₁ ∷ l₂₂) ⟩
+        ((l'₁₁ ++ a'₁ ∷ l'₁₂) ++ a' ∷ l'₂) ++ a₁ ∷ l₂₂
+      ≡⟨ Eq.cong₂ _++_ l≡l₁++a∷l₂₁ refl ⟩
+        (l₁ ++ a ∷ l₂₁) ++ a₁ ∷ l₂₂
+      ≡⟨ List.++-assoc l₁ (a ∷ l₂₁) (a₁ ∷ l₂₂) ⟩
+        l₁ ++ a ∷ l₂₁ ++ a₁ ∷ l₂₂
+      ∎) ,
+    (valid (red (black t'₁₁ a'₁ t'₁₂) a' (black t'₂ a₁ t₂₂)))))
+      where open ≡-Reasoning
+joinLeftContCase₂ {A} l₁ l₂₁ l₂₂ a a₁ y₂₁ y₂₂ n₂ t₂₂ (l , l≡l₁++a∷l₂₁ , valid t') =
+  ret (((l₁ ++ [ a ] ++ l₂₁) ++ [ a₁ ] ++ l₂₂) ,
+    (List.++-assoc l₁ (a ∷ l₂₁) (a₁ ∷ l₂₂) ,
+    Eq.subst (λ l' → AlmostLeftRBT A black (suc n₂) l') (Eq.cong₂ _++_ l≡l₁++a∷l₂₁ refl) (valid (black t' a₁ t₂₂))))
+
+joinLeft :
+  cmp
+    ( Π color λ y₁ → Π nat λ n₁ → Π (list A) λ l₁ → Π (irbt A y₁ n₁ l₁) λ _ →
+      Π A λ a →
+      Π color λ y₂ → Π nat λ n₂ → Π (list A) λ l₂ → Π (irbt A y₂ n₂ l₂) λ _ →
+      Π (meta⁺ (n₁ < n₂)) λ _ →
+      F (Σ⁺ (list A) λ l → (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ (alrbt A y₂ n₂ l))
+    )
+joinLeft {A} y₁ n₁ l₁ t₁ a .red n₂ l₂ (red {l₁ = l₂₁} {l₂ = l₂₂} t₂₁ a₁ t₂₂) n₁<n₂ =
+  step (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ l₁ ++ a ∷ l₂₁ ++ a₁ ∷ l₂₂)) ×⁺ (alrbt A red n₂ l)))) (1 , 1) $
+  bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ l₁ ++ a ∷ l₂₁ ++ a₁ ∷ l₂₂)) ×⁺ (alrbt A red n₂ l))))
+    (joinLeft _ _ _ t₁ a _ _ _ t₂₁ n₁<n₂)
+    (joinLeftContCase₁ l₁ l₂₁ l₂₂ a a₁ n₂ t₂₂)
+joinLeft {A} y₁ n₁ l₁ t₁ a .black (suc n₂) l₂ (black {y₁ = y₂₁} {y₂ = y₂₂} {l₁ = l₂₁} {l₂ = l₂₂} t₂₁ a₁ t₂₂) n₁<n₂ with n₁ Nat.≟ n₂
+joinLeft {A} red n₁ l₁ (red {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a .black (suc n₁) l₂ (black {l₁ = l₂₁} {l₂ = l₂₂} t₂₁ a₂ t₂₂) n₁<n₂ | yes refl =
+  ret (((l₁₁ ++ [ a₁ ] ++ l₁₂) ++ [ a ] ++ (l₂₁ ++ [ a₂ ] ++ l₂₂)) ,
+    (refl ,
+    valid (red (black t₁₁ a₁ t₁₂) a (black t₂₁ a₂ t₂₂))))
+joinLeft {A} black n₁ l₁ t₁ a .black (suc n₂) l₂ (black {y₁ = red} {l₂ = l₂₂} (red {l₁ = l₂₁₁} {l₂ = l₂₁₂} t₂₁₁ a₁₁ t₂₁₂) a₁ t₂₂) n₁<n₂ | yes refl =
+  ret (((l₁ ++ [ a ] ++ l₂₁₁) ++ [ a₁₁ ] ++ (l₂₁₂ ++ [ a₁ ] ++ l₂₂)) ,
+    ((begin
+      (l₁ ++ [ a ] ++ l₂₁₁) ++ [ a₁₁ ] ++ l₂₁₂ ++ [ a₁ ] ++ l₂₂
+    ≡⟨ List.++-assoc l₁ (a ∷ l₂₁₁) (a₁₁ ∷ l₂₁₂ ++ a₁ ∷ l₂₂) ⟩
+      l₁ ++ a ∷ l₂₁₁ ++ a₁₁ ∷ l₂₁₂ ++ a₁ ∷ l₂₂
+    ≡⟨ Eq.cong₂ _++_ refl (Eq.sym (List.++-assoc (a ∷ l₂₁₁) (a₁₁ ∷ l₂₁₂) (a₁ ∷ l₂₂))) ⟩
+      l₁ ++ a ∷ (l₂₁₁ ++ [ a₁₁ ] ++ l₂₁₂) ++ a₁ ∷ l₂₂
+    ∎) ,
+    (valid (red (black t₁ a t₂₁₁) a₁₁ (black t₂₁₂ a₁ t₂₂)))))
+      where open ≡-Reasoning
+joinLeft {A} black n₁ l₁ t₁ a .black (suc n₂) l₂ (black {y₁ = black} {l₁ = l₂₁} {l₂ = l₂₂} t₂₁ a₁ t₂₂) n₁<n₂ | yes refl =
+  ret (((l₁ ++ [ a ] ++ l₂₁) ++ [ a₁ ] ++ l₂₂) ,
+    ((List.++-assoc l₁ (a ∷ l₂₁) (a₁ ∷ l₂₂)) ,
+    (valid (black (red t₁ a t₂₁) a₁ t₂₂))))
+... | no n₁≢n₂ =
+  step (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ l₁ ++ a ∷ l₂₁ ++ a₁ ∷ l₂₂)) ×⁺ (alrbt A black (suc n₂) l)))) (1 , 1) $
+  bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ l₁ ++ a ∷ l₂₁ ++ a₁ ∷ l₂₂)) ×⁺ (alrbt A black (suc n₂) l))))
+    (joinLeft _ _ _ t₁ a _ _ _ t₂₁ (Nat.≤∧≢⇒< (Nat.≤-pred n₁<n₂) n₁≢n₂))
+    (joinLeftContCase₂ l₁ l₂₁ l₂₂ a a₁ y₂₁ y₂₂ n₂ t₂₂)
+
+joinLeft/cost : (y : val color) (n₁ n₂ : val nat) → ℂ
+joinLeft/cost red n₁ n₂ = (1 + (2 * (n₂ ∸ n₁)) , 1 + (2 * (n₂ ∸ n₁)))
+joinLeft/cost black n₁ n₂ = ((2 * (n₂ ∸ n₁)) , (2 * (n₂ ∸ n₁)))
+
+joinLeft/is-bounded' : ∀ y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁<n₂
+  → IsBounded (Σ⁺ (list A) λ l → (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ (alrbt A y₂ n₂ l)) (joinLeft y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁<n₂) (joinLeft/cost y₂ n₁ n₂)
+
+joinLeft/is-bounded : ∀ {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁<n₂
+  → IsBounded (Σ⁺ (list A) λ l → (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ (alrbt A y₂ n₂ l)) (joinLeft y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁<n₂) (1 + (2 * (n₂ ∸ n₁)) , 1 + (2 * (n₂ ∸ n₁)))
+
+joinLeft/is-bounded' {A} y₁ n₁ l₁ t₁ a .red n₂ l₂ (red {l₁ = l₂₁} {l₂ = l₂₂} t₂₁ a₁ t₂₂) n₁<n₂ =
+  let open ≤⁻-Reasoning cost in
+    begin
+      step cost (1 , 1) (
+        bind cost (
+          bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ l₁ ++ a ∷ l₂₁ ++ a₁ ∷ l₂₂)) ×⁺ (alrbt A red n₂ l))))
+            (joinLeft _ _ _ t₁ a _ _ _ t₂₁ n₁<n₂)
+            (joinLeftContCase₁ l₁ l₂₁ l₂₂ a a₁ n₂ t₂₂))
+        (λ _ → ret triv))
+    ≡⟨ Eq.cong
+         (λ e → step cost (1 , 1) e)
+         (Eq.cong
+            (λ f → bind cost (joinLeft _ _ _ t₁ a _ _ _ t₂₁ n₁<n₂) f)
+            (funext λ { (_ , _ , valid {y = red} _) → refl
+                      ; (_ , _ , valid {y = black} _) → refl })) ⟩
+      step cost (1 , 1) (
+        bind cost (joinLeft _ _ _ t₁ a _ _ _ t₂₁ n₁<n₂)
+        (λ _ → ret triv))
+    ≤⟨ ≤⁻-mono (λ e → step cost (1 , 1) e) (joinLeft/is-bounded' _ _ _ t₁ a _ _ _ t₂₁ n₁<n₂) ⟩
+      step cost (1 , 1) (
+        bind cost (step⋆ (2 * (n₂ ∸ n₁) , 2 * (n₂ ∸ n₁))) λ _ → ret triv)
+    ≤⟨ ≤⁻-refl ⟩
+      step⋆ (1 + 2 * (n₂ ∸ n₁) , 1 + 2 * (n₂ ∸ n₁))
+    ∎
+joinLeft/is-bounded' {A} y₁ n₁ l₁ t₁ a .black (suc n₂) l₂ (black {y₁ = y₂₁} {y₂ = y₂₂} {l₁ = l₂₁} {l₂ = l₂₂} t₂₁ a₁ t₂₂) n₁<n₂ with n₁ Nat.≟ n₂
+joinLeft/is-bounded' red n₁ _ (red _ _ _) _ .black _ _ (black _ _ _) _ | yes refl =
+  step⋆-mono-≤⁻ (Nat.z≤n {2 * (suc n₁ ∸ n₁)} , Nat.z≤n {2 * (suc n₁ ∸ n₁)})
+joinLeft/is-bounded' black n₁ _ _ _ .black _ _ (black {y₁ = red} (red _ _ _) _ _) _ | yes refl =
+  step⋆-mono-≤⁻ (Nat.z≤n {2 * (suc n₁ ∸ n₁)} , Nat.z≤n {2 * (suc n₁ ∸ n₁)})
+joinLeft/is-bounded' black n₁ _ _ _ .black _ _ (black {y₁ = black} _ _ _) _ | yes refl =
+  step⋆-mono-≤⁻ (Nat.z≤n {2 * (suc n₁ ∸ n₁)} , Nat.z≤n {2 * (suc n₁ ∸ n₁)})
+...| no n₁≢n₂ =
+  let open ≤⁻-Reasoning cost in
+    begin
+      step cost (1 , 1) (
+        bind cost (
+          bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ l₁ ++ a ∷ l₂₁ ++ a₁ ∷ l₂₂)) ×⁺ (alrbt A black (suc n₂) l))))
+            (joinLeft _ _ _ t₁ a _ _ _ t₂₁ (Nat.≤∧≢⇒< (Nat.≤-pred n₁<n₂) n₁≢n₂))
+            (joinLeftContCase₂ l₁ l₂₁ l₂₂ a a₁ y₂₁ y₂₂ n₂ t₂₂))
+        (λ _ → ret triv))
+    ≡⟨ Eq.cong
+         (λ e → step cost (1 , 1) e)
+         (Eq.cong
+           (λ f → bind cost (joinLeft _ _ _ t₁ a _ _ _ t₂₁ (Nat.≤∧≢⇒< (Nat.≤-pred n₁<n₂) n₁≢n₂)) f)
+           (funext (λ { (_ , _ , violation (red _ _ _) _ _) → refl
+                      ; (_ , _ , valid _) → refl }))) ⟩
+      step cost (1 , 1) (
+        bind cost (joinLeft _ _ _ t₁ a _ _ _ t₂₁ (Nat.≤∧≢⇒< (Nat.≤-pred n₁<n₂) n₁≢n₂))
+        (λ _ → ret triv))
+    ≤⟨ ≤⁻-mono (λ e → step cost (1 , 1) e) (joinLeft/is-bounded _ _ _ t₁ a _ _ _ t₂₁ _) ⟩
+      step cost (1 , 1) (
+        bind cost (step⋆ (1 + 2 * (n₂ ∸ n₁) , 1 + 2 * (n₂ ∸ n₁))) λ _ → ret triv)
+    ≡⟨ Eq.cong (λ c → step⋆ c)
+         (Eq.cong₂ _,_
+           (Eq.trans (Eq.sym (Nat.*-suc 2 (n₂ ∸ n₁))) (Eq.cong (2 *_) (Eq.sym (Nat.+-∸-assoc 1 (Nat.≤-pred n₁<n₂)))))
+           (Eq.trans (Eq.sym (Nat.*-suc 2 (n₂ ∸ n₁))) (Eq.cong (2 *_) (Eq.sym (Nat.+-∸-assoc 1 (Nat.≤-pred n₁<n₂)))))) ⟩
+      step⋆ (2 * (suc n₂ ∸ n₁) , 2 * (suc n₂ ∸ n₁))
+    ∎
+
+joinLeft/is-bounded y₁ n₁ l₁ t₁ a red n₂ l₂ t₂ n₁<n₂ =
+  joinLeft/is-bounded' y₁ n₁ l₁ t₁ a red n₂ l₂ t₂ n₁<n₂
+joinLeft/is-bounded y₁ n₁ l₁ t₁ a black n₂ l₂ t₂ n₁<n₂ =
+  let open ≤⁻-Reasoning cost in
+    begin
+      bind cost (joinLeft y₁ n₁ l₁ t₁ a black n₂ l₂ t₂ n₁<n₂) (λ _ → ret triv)
+    ≤⟨ joinLeft/is-bounded' y₁ n₁ l₁ t₁ a black n₂ l₂ t₂ n₁<n₂ ⟩
+      step⋆ (2 * (n₂ ∸ n₁) , 2 * (n₂ ∸ n₁))
+    ≤⟨ step⋆-mono-≤⁻ (Nat.n≤1+n _ , Nat.n≤1+n _) ⟩
+      step⋆ (1 + 2 * (n₂ ∸ n₁) , 1 + 2 * (n₂ ∸ n₁))
+    ∎
+
+data AlmostRightRBT (A : tp⁺) : (left-color : val color) → val nat → val (list A) → Set where
+  violation :
+    {n : val nat} {l₁ l₂ : val (list A)}
+    → IRBT A black n l₁ → (a : val A) → IRBT A red n l₂
+    → AlmostRightRBT A red n (l₁ ++ [ a ] ++ l₂)
+  valid :
+    {left-color : val color} {n : val nat} {y : val color} {l : val (list A)} → IRBT A y n l
+    → AlmostRightRBT A left-color n l
+arrbt : (A : tp⁺) → val color → val nat → val (list A) → tp⁺
+arrbt A y n l = meta⁺ (AlmostRightRBT A y n l)
+
+joinRightContCase₁ : ∀ l₁₁ l₁₂ l₂ a a₁ n₁ t₁₁ →
+  (Σ (List (val A)) (λ a₂ → Σ (a₂ ≡ l₁₂ ++ a ∷ l₂) (λ x → AlmostRightRBT A black n₁ a₂))) →
+    cmp (F (Σ⁺ (list A) (λ l → meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂) ×⁺ arrbt A red n₁ l)))
+joinRightContCase₁ {A} l₁₁ l₁₂ l₂ a a₁ n₁ t₁₁ (l , l≡l₁₂++a₁∷l₂ , valid {y = red} t') =
+  ret (l₁₁ ++ [ a₁ ] ++ (l₁₂ ++ [ a ] ++ l₂) ,
+    Eq.sym (List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂)) ,
+    Eq.subst (λ l' → AlmostRightRBT A red n₁ l') (Eq.cong₂ _++_ refl (Eq.cong₂ _∷_ refl l≡l₁₂++a₁∷l₂)) (violation t₁₁ a₁ t'))
+joinRightContCase₁ {A} l₁₁ l₁₂ l₂ a a₁ n₁ t₁₁ (l , l≡l₁₂++a₁∷l₂ , valid {y = black} t') =
+  ret (l₁₁ ++ [ a₁ ] ++ (l₁₂ ++ [ a ] ++ l₂) ,
+    Eq.sym (List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂)) ,
+    Eq.subst (λ l' → AlmostRightRBT A red n₁ l') (Eq.cong₂ _++_ refl (Eq.cong₂ _∷_ refl l≡l₁₂++a₁∷l₂)) (valid (red t₁₁ a₁ t')))
+
+joinRightContCase₂ : ∀ l₁₁ l₁₂ l₂ a a₁ y₁₁ y₁₂ n₁ (t₁₁ : IRBT A y₁₁ n₁ l₁₁) →
+  (Σ (List (val A)) (λ a₂ → Σ (a₂ ≡ l₁₂ ++ a ∷ l₂) (λ x → AlmostRightRBT A y₁₂ n₁ a₂))) →
+    cmp (F (Σ⁺ (list A) (λ l → meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂) ×⁺ arrbt A black (suc n₁) l)))
+joinRightContCase₂ {A} l₁₁ l₁₂ l₂ a a₁ y₁₁ y₁₂ n₁ t₁₁ (l , l≡l₁₂++a∷l₂ , violation {l₁ = l'₁} t'₁ a' (red {l₁ = l'₂₁} {l₂ = l'₂₂} t'₂₁ a'₂ t'₂₂)) =
+  ret ((l₁₁ ++ [ a₁ ] ++ l'₁) ++ [ a' ] ++ (l'₂₁ ++ [ a'₂ ] ++ l'₂₂) ,
+    (begin
+      (l₁₁ ++ a₁ ∷ l'₁) ++ a' ∷ l'₂₁ ++ a'₂ ∷ l'₂₂
+    ≡⟨ List.++-assoc l₁₁ (a₁ ∷ l'₁) (a' ∷ l'₂₁ ++ a'₂ ∷ l'₂₂) ⟩
+      l₁₁ ++ a₁ ∷ l'₁ ++ a' ∷ l'₂₁ ++ a'₂ ∷ l'₂₂
+    ≡⟨ Eq.cong₂ _++_ refl (Eq.cong₂ _∷_ refl l≡l₁₂++a∷l₂) ⟩
+      l₁₁ ++ a₁ ∷ l₁₂ ++ a ∷ l₂
+    ≡˘⟨ List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂) ⟩
+      (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂
+    ∎) ,
+    (valid (red (black t₁₁ a₁ t'₁) a' (black t'₂₁ a'₂ t'₂₂))))
+      where open ≡-Reasoning
+joinRightContCase₂ {A} l₁₁ l₁₂ l₂ a a₁ y₁₁ y₁₂ n₁ t₁₁(l , l≡l₁₂++a∷l₂ , valid t') =
+  ret (l₁₁ ++ [ a₁ ] ++ (l₁₂ ++ [ a ] ++ l₂) ,
+    Eq.sym (List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂)) ,
+    Eq.subst (λ l' → AlmostRightRBT A black (suc n₁) l') (Eq.cong₂ _++_ refl (Eq.cong₂ _∷_ refl l≡l₁₂++a∷l₂)) (valid (black t₁₁ a₁ t')))
+
+joinRight :
+  cmp
+    ( Π color λ y₁ → Π nat λ n₁ → Π (list A) λ l₁ → Π (irbt A y₁ n₁ l₁) λ _ →
+      Π A λ a →
+      Π color λ y₂ → Π nat λ n₂ → Π (list A) λ l₂ → Π (irbt A y₂ n₂ l₂) λ _ →
+      Π (meta⁺ (n₁ > n₂)) λ _ →
+      F (Σ⁺ (list A) λ l → (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ (arrbt A y₁ n₁ l))
+    )
+joinRight {A} .red n₁ l₁ (red {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ =
+  step (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A red n₁ l)))) (1 , 1) $
+  bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A red n₁ l))))
+    (joinRight _ _ _ t₁₂ a _ _ _ t₂ n₁>n₂)
+    (joinRightContCase₁ l₁₁ l₁₂ l₂ a a₁ n₁ t₁₁)
+joinRight {A} .black (suc n₁) l₁ (black {y₁ = y₁₁} {y₂ = y₁₂} {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ with n₁ Nat.≟ n₂
+joinRight {A} .black (suc n₁) l₁ (black {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a red n₁ l₂ (red {l₁ = l₂₁} {l₂ = l₂₂} t₂₁ a₂ t₂₂) n₁>n₂ | yes refl =
+  ret ((l₁₁ ++ [ a₁ ] ++ l₁₂) ++ [ a ] ++ (l₂₁ ++ [ a₂ ] ++ l₂₂) ,
+    refl ,
+    valid (red (black t₁₁ a₁ t₁₂) a (black t₂₁ a₂ t₂₂)))
+joinRight {A} .black (suc n₁) l₁ (black {y₂ = red} {l₁ = l₁₁} t₁₁ a₁ (red {l₁ = l₁₂₁} {l₂ = l₁₂₂} t₁₂₁ a₁₂ t₁₂₂)) a black n₁ l₂ t₂ n₁>n₂ | yes refl =
+  ret ((l₁₁ ++ [ a₁ ] ++ l₁₂₁) ++ [ a₁₂ ] ++ (l₁₂₂ ++ [ a ] ++ l₂) ,
+    (begin
+      (l₁₁ ++ a₁ ∷ l₁₂₁) ++ a₁₂ ∷ l₁₂₂ ++ a ∷ l₂
+    ≡⟨ List.++-assoc l₁₁ (a₁ ∷ l₁₂₁) (a₁₂ ∷ l₁₂₂ ++ a ∷ l₂) ⟩
+      l₁₁ ++ a₁ ∷ l₁₂₁ ++ a₁₂ ∷ l₁₂₂ ++ a ∷ l₂
+    ≡⟨ Eq.cong₂ _++_ refl (Eq.sym (List.++-assoc (a₁ ∷ l₁₂₁) (a₁₂ ∷ l₁₂₂) (a ∷ l₂))) ⟩
+      l₁₁ ++ (a₁ ∷ l₁₂₁ ++ a₁₂ ∷ l₁₂₂) ++ a ∷ l₂
+    ≡˘⟨ List.++-assoc l₁₁ (a₁ ∷ l₁₂₁ ++ a₁₂ ∷ l₁₂₂) (a ∷ l₂) ⟩
+      (l₁₁ ++ a₁ ∷ l₁₂₁ ++ a₁₂ ∷ l₁₂₂) ++ a ∷ l₂
+    ∎) ,
+    valid (red (black t₁₁ a₁ t₁₂₁) a₁₂ (black t₁₂₂ a t₂)))
+      where open ≡-Reasoning
+joinRight {A} .black (suc n₁) l₁ (black {y₂ = black} {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a black n₁ l₂ t₂ n₁>n₂ | yes refl =
+  ret (l₁₁ ++ [ a₁ ] ++ (l₁₂ ++ [ a ] ++ l₂) ,
+    Eq.sym (List.++-assoc l₁₁ (a₁ ∷ l₁₂) (a ∷ l₂)) ,
+    valid (black t₁₁ a₁ (red t₁₂ a t₂)))
+... | no n₁≢n₂ =
+  step (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A black (suc n₁) l)))) (1 , 1) $
+  bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A black (suc n₁) l))))
+    (joinRight _ _ _ t₁₂ a _ _ _ t₂ (Nat.≤∧≢⇒< (Nat.≤-pred n₁>n₂) (≢-sym n₁≢n₂)))
+    (joinRightContCase₂ l₁₁ l₁₂ l₂ a a₁ y₁₁ y₁₂ n₁ t₁₁)
+
+joinRight/cost : (y : val color) (n₁ n₂ : val nat) → ℂ
+joinRight/cost red n₁ n₂ = 1 + (2 * (n₁ ∸ n₂)) , 1 + (2 * (n₁ ∸ n₂))
+joinRight/cost black n₁ n₂ = (2 * (n₁ ∸ n₂)) , (2 * (n₁ ∸ n₂))
+
+joinRight/is-bounded' : ∀ y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂
+  → IsBounded (Σ⁺ (list A) λ l → (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ (arrbt A y₁ n₁ l)) (joinRight y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂) (joinRight/cost y₁ n₁ n₂)
+
+joinRight/is-bounded : ∀ {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂
+  → IsBounded (Σ⁺ (list A) λ l → (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ (arrbt A y₁ n₁ l)) (joinRight y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂) (1 + (2 * (n₁ ∸ n₂)) , 1 + (2 * (n₁ ∸ n₂)))
+
+joinRight/is-bounded' {A} red n₁ l₁ (red {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ =
+  let open ≤⁻-Reasoning cost in
+    begin
+      step cost (1 , 1) (
+        bind cost (
+          bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A red n₁ l))))
+            (joinRight _ _ _ t₁₂ a _ _ _ t₂ n₁>n₂)
+            (joinRightContCase₁ l₁₁ l₁₂ l₂ a a₁ n₁ t₁₁))
+        (λ _ → ret triv))
+    ≡⟨ Eq.cong
+         (λ e → step cost (1 , 1) e)
+         (Eq.cong
+           (λ f → bind cost (joinRight _ _ _ t₁₂ a _ _ _ t₂ n₁>n₂) f)
+           (funext ((λ { (_ , _ , valid {y = red} _) → refl
+                       ; (_ , _ , valid {y = black} _) → refl })))) ⟩
+      step cost (1 , 1) (
+        bind cost (joinRight _ _ _ t₁₂ a _ _ _ t₂ n₁>n₂)
+        (λ _ → ret triv))
+    ≤⟨ ≤⁻-mono (λ e → step cost (1 , 1) e) (joinRight/is-bounded' _ _ _ t₁₂ a _ _ _ t₂ n₁>n₂) ⟩
+      step cost (1 , 1) (
+        bind cost (step⋆ (2 * (n₁ ∸ n₂) , 2 * (n₁ ∸ n₂))) λ _ → ret triv)
+    ≤⟨ ≤⁻-refl ⟩
+      step⋆ (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂))
+    ∎
+joinRight/is-bounded' {A} black (suc n₁) l₁ (black {y₁ = y₁₁} {y₂ = y₁₂} {l₁ = l₁₁} {l₂ = l₁₂} t₁₁ a₁ t₁₂) a y₂ n₂ l₂ t₂ n₁>n₂ with n₁ Nat.≟ n₂
+joinRight/is-bounded' black n₁ _ (black _ _ _) _ red _ _ (red _ _ _) _ | yes refl =
+  step⋆-mono-≤⁻ (Nat.z≤n {2 * (suc n₁ ∸ n₁)} , Nat.z≤n {2 * (suc n₁ ∸ n₁)})
+joinRight/is-bounded' black n₁ _ (black {y₂ = red} _ _ (red _ _ _)) _ black _ _ _ _ | yes refl =
+  step⋆-mono-≤⁻ (Nat.z≤n {2 * (suc n₁ ∸ n₁)} , Nat.z≤n {2 * (suc n₁ ∸ n₁)})
+joinRight/is-bounded' black n₁ _ (black {y₂ = black} _ _ _) _ black _ _ _ _ | yes refl =
+  step⋆-mono-≤⁻ (Nat.z≤n {2 * (suc n₁ ∸ n₁)} , Nat.z≤n {2 * (suc n₁ ∸ n₁)})
+... | no n₁≢n₂ =
+  let open ≤⁻-Reasoning cost in
+    begin
+      step cost (1 , 1) (
+        bind cost (
+          bind (F (Σ⁺ (list A) (λ l → (meta⁺ (l ≡ (l₁₁ ++ a₁ ∷ l₁₂) ++ a ∷ l₂)) ×⁺ (arrbt A black (suc n₁) l))))
+            (joinRight _ _ _ t₁₂ a _ _ _ t₂ (Nat.≤∧≢⇒< (Nat.≤-pred n₁>n₂) (≢-sym n₁≢n₂)))
+            (joinRightContCase₂ l₁₁ l₁₂ l₂ a a₁ y₁₁ y₁₂ n₁ t₁₁))
+        (λ _ → ret triv))
+    ≡⟨ Eq.cong
+        (λ e → step cost (1 , 1) e)
+          (Eq.cong
+            (λ f → bind cost (joinRight _ _ _ t₁₂ a _ _ _ t₂ (Nat.≤∧≢⇒< (Nat.≤-pred n₁>n₂) (≢-sym n₁≢n₂))) f)
+            (funext (λ { (_ , _ , violation _ _ (red _ _ _)) → refl
+                       ; (_ , _ , valid _) → refl }))) ⟩
+      step cost (1 , 1) (
+        bind cost (joinRight _ _ _ t₁₂ a _ _ _ t₂ (Nat.≤∧≢⇒< (Nat.≤-pred n₁>n₂) (≢-sym n₁≢n₂)))
+        (λ _ → ret triv))
+    ≤⟨ ≤⁻-mono (λ e → step cost (1 , 1) e) (joinRight/is-bounded _ _ _ t₁₂ a _ _ _ t₂ _) ⟩
+      step cost (1 , 1) (
+        bind cost (step⋆ (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂))) λ _ → ret triv)
+    ≡⟨ Eq.cong (λ c → step⋆ c)
+         (Eq.cong₂ _,_
+           (Eq.trans (Eq.sym (Nat.*-suc 2 (n₁ ∸ n₂))) (Eq.cong (2 *_) (Eq.sym (Nat.+-∸-assoc 1 n₁>n₂))))
+           (Eq.trans (Eq.sym (Nat.*-suc 2 (n₁ ∸ n₂))) (Eq.cong (2 *_) (Eq.sym (Nat.+-∸-assoc 1 n₁>n₂))))) ⟩
+      step⋆ (2 * (suc n₁ ∸ n₂) , 2 * (suc n₁ ∸ n₂))
+    ∎
+
+joinRight/is-bounded red n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ =
+  joinRight/is-bounded' red n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂
+joinRight/is-bounded black n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ =
+  let open ≤⁻-Reasoning cost in
+    begin
+      bind cost (joinRight black n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂) (λ _ → ret triv)
+    ≤⟨ joinRight/is-bounded' black n₁ l₁ t₁ a y₂ n₂ l₂ t₂ n₁>n₂ ⟩
+      step⋆ (2 * (n₁ ∸ n₂) , 2 * (n₁ ∸ n₂))
+    ≤⟨ step⋆-mono-≤⁻ (Nat.n≤1+n _ , Nat.n≤1+n _) ⟩
+      step⋆ (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂))
+    ∎
+
+i-joinContCaseLeft : ∀ l₁ l₂ a y₂ n₁ n₂ n₁<n₂ →
+  (Σ (List (val A)) (λ a₁ → Σ (a₁ ≡ l₁ ++ a ∷ l₂) (λ x → AlmostLeftRBT A y₂ n₂ a₁))) →
+    cmp (F (Σ⁺ color (λ y → Σ⁺ (list A) (λ l → meta⁺ (l ≡ l₁ ++ a ∷ l₂) ×⁺ (irbt A y (suc (n₁ ⊔ n₂)) l ⊎⁺ irbt A y (n₁ ⊔ n₂) l)))))
+i-joinContCaseLeft {A} l₁ l₂ a y₂ n₁ n₂ n₁<n₂ (l , l≡l₁++a∷l₂ , violation {l₁ = l'₁} {l₂ = l'₂} t'₁ a' t'₂) =
+  ret (black , l'₁ ++ [ a' ] ++ l'₂ , l≡l₁++a∷l₂ ,
+    inj₁ (Eq.subst (λ n → IRBT A black (suc n) (l'₁ ++ a' ∷ l'₂)) (Eq.sym (Nat.m≤n⇒m⊔n≡n (Nat.<⇒≤ n₁<n₂)))
+    (black t'₁ a' t'₂)))
+i-joinContCaseLeft {A} l₁ l₂ a y₂ n₁ n₂ n₁<n₂ (l , l≡l₁++a∷l₂ , valid {n = n} {y = y} {l = l} t') =
+  ret (y , l , l≡l₁++a∷l₂ , inj₂ (Eq.subst (λ n → IRBT A y n l) (Eq.sym (Nat.m≤n⇒m⊔n≡n (Nat.<⇒≤ n₁<n₂))) t'))
+
+i-joinContCaseRight : ∀ l₁ l₂ a y₁ n₁ n₂ n₁>n₂ →
+  (Σ (List (val A)) (λ a₁ → Σ (a₁ ≡ l₁ ++ a ∷ l₂) (λ x → AlmostRightRBT A y₁ n₁ a₁))) →
+    cmp (F (Σ⁺ color (λ y → Σ⁺ (list A) (λ l → meta⁺ (l ≡ l₁ ++ a ∷ l₂) ×⁺ (irbt A y (suc (n₁ ⊔ n₂)) l ⊎⁺ irbt A y (n₁ ⊔ n₂) l)))))
+i-joinContCaseRight {A} l₁ l₂ a y₁ n₁ n₂ n₁>n₂ (l , l≡l₁++a∷l₂ , violation {l₁ = l'₁} {l₂ = l'₂} t'₁ a' t'₂) =
+  ret (black , l'₁ ++ [ a' ] ++ l'₂ , l≡l₁++a∷l₂ ,
+    inj₁ (Eq.subst (λ n → IRBT A black (suc n) (l'₁ ++ a' ∷ l'₂)) (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂)))
+    (black t'₁ a' t'₂)))
+i-joinContCaseRight {A} l₁ l₂ a y₁ n₁ n₂ n₁>n₂ (l , l≡l₁++a∷l₂ , valid {n = n} {y = y} {l = l} t') =
+  ret (y , l , l≡l₁++a∷l₂ , inj₂ (Eq.subst (λ n → IRBT A y n l) (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) t'))
+
+i-join :
+  cmp
+    ( Π color λ y₁ → Π nat λ n₁ → Π (list A) λ l₁ → Π (irbt A y₁ n₁ l₁) λ _ →
+      Π A λ a →
+      Π color λ y₂ → Π nat λ n₂ → Π (list A) λ l₂ → Π (irbt A y₂ n₂ l₂) λ _ →
+      F (Σ⁺ color λ y → Σ⁺ (list A) λ l →
+        (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ ((irbt A y (1 + (n₁ Nat.⊔ n₂)) l) ⊎⁺ (irbt A y (n₁ Nat.⊔ n₂) l)))
+    )
+i-join {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ with Nat.<-cmp n₁ n₂
+i-join {A} red n₁ l₁ t₁ a y₂ n₂ l₂ t₂ | tri≈ ¬n₁<n₂ refl ¬n₁>n₂ =
+  ret (black , l₁ ++ [ a ] ++ l₂ , refl ,
+    inj₁ (Eq.subst (λ n → IRBT A black (suc n) (l₁ ++ a ∷ l₂)) (Eq.sym (Nat.⊔-idem n₁)) (black t₁ a t₂)))
+i-join {A} black n₁ l₁ t₁ a red n₂ l₂ t₂ | tri≈ ¬n₁<n₂ refl ¬n₁>n₂ =
+  ret (black , l₁ ++ [ a ] ++ l₂ , refl ,
+    inj₁ (Eq.subst (λ n → IRBT A black (suc n) (l₁ ++ a ∷ l₂)) (Eq.sym (Nat.⊔-idem n₁)) (black t₁ a t₂)))
+i-join {A} black n₁ l₁ t₁ a black n₂ l₂ t₂ | tri≈ ¬n₁<n₂ refl ¬n₁>n₂ =
+  ret (red , l₁ ++ [ a ] ++ l₂ , refl ,
+    inj₂ (Eq.subst (λ n → IRBT A red n (l₁ ++ a ∷ l₂)) (Eq.sym (Nat.⊔-idem n₁)) (red t₁ a t₂)))
+... | tri< n₁<n₂ n₁≢n₂ ¬n₁>n₂ =
+  bind (F (Σ⁺ color λ y → Σ⁺ (list A) λ l →
+        (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ ((irbt A y (1 + (n₁ Nat.⊔ n₂)) l) ⊎⁺ (irbt A y (n₁ Nat.⊔ n₂) l))))
+    (joinLeft _ _ _ t₁ a _ _ _ t₂ n₁<n₂)
+    (i-joinContCaseLeft l₁ l₂ a y₂ n₁ n₂ n₁<n₂)
+... | tri> ¬n₁<n₂ n₁≢n₂ n₁>n₂ =
+  bind (F (Σ⁺ color λ y → Σ⁺ (list A) λ l →
+        (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ ((irbt A y (1 + (n₁ Nat.⊔ n₂)) l) ⊎⁺ (irbt A y (n₁ Nat.⊔ n₂) l))))
+    (joinRight _ _ _ t₁ a _ _ _ t₂ n₁>n₂)
+    (i-joinContCaseRight l₁ l₂ a y₁ n₁ n₂ n₁>n₂)
+
+i-join/is-bounded : ∀ {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂
+  → IsBounded (Σ⁺ color λ y → Σ⁺ (list A) λ l →
+        (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ ((irbt A y (1 + (n₁ Nat.⊔ n₂)) l) ⊎⁺ (irbt A y (n₁ Nat.⊔ n₂) l))) (i-join y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂)
+          (1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂)) , 1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂)))
+i-join/is-bounded {A} y₁ n₁ l₁ t₁ a y₂ n₂ l₂ t₂ with Nat.<-cmp n₁ n₂
+i-join/is-bounded {A} red n₁ l₁ t₁ a y₂ .n₁ l₂ t₂ | tri≈ ¬n₁<n₂ refl ¬n₁>n₂ =
+  step⋆-mono-≤⁻ (Nat.z≤n {1 + (2 * (n₁ Nat.⊔ n₁ ∸ n₁ Nat.⊓ n₁))}, Nat.z≤n {1 + (2 * (n₁ Nat.⊔ n₁ ∸ n₁ Nat.⊓ n₁))})
+i-join/is-bounded {A} black n₁ l₁ t₁ a red n₁ l₂ t₂ | tri≈ ¬n₁<n₂ refl ¬n₁>n₂ =
+  step⋆-mono-≤⁻ (Nat.z≤n {1 + (2 * (n₁ Nat.⊔ n₁ ∸ n₁ Nat.⊓ n₁))}, Nat.z≤n {1 + (2 * (n₁ Nat.⊔ n₁ ∸ n₁ Nat.⊓ n₁))})
+i-join/is-bounded {A} black n₁ l₁ t₁ a black n₁ l₂ t₂ | tri≈ ¬n₁<n₂ refl ¬n₁>n₂ =
+  step⋆-mono-≤⁻ (Nat.z≤n {1 + (2 * (n₁ Nat.⊔ n₁ ∸ n₁ Nat.⊓ n₁))}, Nat.z≤n {1 + (2 * (n₁ Nat.⊔ n₁ ∸ n₁ Nat.⊓ n₁))})
+... | tri< n₁<n₂ n₁≢n₂ ¬n₁>n₂ =
+  let open ≤⁻-Reasoning cost in
+    begin
+      bind cost (
+        bind (F (Σ⁺ color λ y → Σ⁺ (list A) λ l →
+          (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ ((irbt A y (1 + (n₁ Nat.⊔ n₂)) l) ⊎⁺ (irbt A y (n₁ Nat.⊔ n₂) l))))
+            (joinLeft _ _ _ t₁ a _ _ _ t₂ n₁<n₂)
+            (i-joinContCaseLeft l₁ l₂ a y₂ n₁ n₂ n₁<n₂))
+      (λ _ → ret triv)
+    ≡⟨ Eq.cong
+         (λ f → bind cost (joinLeft _ _ _ t₁ a _ _ _ t₂ n₁<n₂) f)
+         (funext (λ { (_ , _ , violation _ _ _) → refl
+                    ; (_ , _ , valid _) → refl })) ⟩
+      bind cost (joinLeft _ _ _ t₁ a _ _ _ t₂ n₁<n₂) (λ _ → ret triv)
+    ≤⟨ joinLeft/is-bounded _ _ _ t₁ a _ _ _ t₂ n₁<n₂ ⟩
+      step⋆ (1 + 2 * (n₂ ∸ n₁) , 1 + 2 * (n₂ ∸ n₁))
+    ≡⟨ Eq.cong (λ c → step⋆ c)
+         (Eq.cong₂ _,_
+           (Eq.cong (1 +_) (Eq.cong (2 *_) (Eq.cong₂ _∸_ (Eq.sym (Nat.m≤n⇒m⊔n≡n (Nat.<⇒≤ n₁<n₂))) (Eq.sym (Nat.m≤n⇒m⊓n≡m (Nat.<⇒≤ n₁<n₂))))))
+           (Eq.cong (1 +_) (Eq.cong (2 *_) (Eq.cong₂ _∸_ (Eq.sym (Nat.m≤n⇒m⊔n≡n (Nat.<⇒≤ n₁<n₂))) (Eq.sym (Nat.m≤n⇒m⊓n≡m (Nat.<⇒≤ n₁<n₂))))))) ⟩
+      step⋆ (1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂)) , 1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂)))
+    ∎
+... | tri> ¬n₁<n₂ n₁≢n₂ n₁>n₂ =
+  let open ≤⁻-Reasoning cost in
+    begin
+      bind cost (
+        bind (F (Σ⁺ color λ y → Σ⁺ (list A) λ l →
+          (meta⁺ (l ≡ l₁ ++ [ a ] ++ l₂)) ×⁺ ((irbt A y (1 + (n₁ Nat.⊔ n₂)) l) ⊎⁺ (irbt A y (n₁ Nat.⊔ n₂) l))))
+            (joinRight _ _ _ t₁ a _ _ _ t₂ n₁>n₂)
+            (i-joinContCaseRight l₁ l₂ a y₁ n₁ n₂ n₁>n₂))
+      (λ _ → ret triv)
+    ≡⟨ Eq.cong
+         (λ f → bind cost (joinRight _ _ _ t₁ a _ _ _ t₂ n₁>n₂) f)
+           (funext (λ { (_ , _ , violation _ _ _) → refl
+                      ; (_ , _ , valid _) → refl })) ⟩
+      bind cost (joinRight _ _ _ t₁ a _ _ _ t₂ n₁>n₂) (λ _ → ret triv)
+    ≤⟨ joinRight/is-bounded _ _ _ t₁ a _ _ _ t₂ n₁>n₂ ⟩
+      step⋆ (1 + 2 * (n₁ ∸ n₂) , 1 + 2 * (n₁ ∸ n₂))
+    ≡⟨ Eq.cong (λ c → step⋆ c)
+         (Eq.cong₂ _,_
+           (Eq.cong (1 +_) (Eq.cong (2 *_) (Eq.cong₂ _∸_ (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) (Eq.sym (Nat.m≥n⇒m⊓n≡n (Nat.<⇒≤ n₁>n₂))))))
+           (Eq.cong (1 +_) (Eq.cong (2 *_) (Eq.cong₂ _∸_ (Eq.sym (Nat.m≥n⇒m⊔n≡m (Nat.<⇒≤ n₁>n₂))) (Eq.sym (Nat.m≥n⇒m⊓n≡n (Nat.<⇒≤ n₁>n₂))))))) ⟩
+      step⋆ (1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂)) , 1 + (2 * (n₁ Nat.⊔ n₂ ∸ n₁ Nat.⊓ n₂)))
+    ∎
+
+i-nodes : {y : val color} {n : val nat} {l : val (list A)} → IRBT A y n l → val nat
+i-nodes leaf = 0
+i-nodes (red t₁ _ t₂) = 1 + (i-nodes t₁) + (i-nodes t₂)
+i-nodes (black t₁ _ t₂) = 1 + (i-nodes t₁) + (i-nodes t₂)
+
+i-nodes≡lengthl : ∀ {y} {n} {l} → (t : IRBT A y n l) → i-nodes t ≡ length l
+i-nodes≡lengthl leaf = refl
+i-nodes≡lengthl (red {l₁ = l₁} {l₂ = l₂} t₁ a t₂) =
+  begin
+    1 + (i-nodes t₁) + (i-nodes t₂)
+  ≡⟨ Eq.cong₂ _+_ (Eq.cong₂ _+_ refl (i-nodes≡lengthl t₁)) (i-nodes≡lengthl t₂) ⟩
+    1 + length l₁ + length l₂
+  ≡⟨ Eq.cong₂ _+_ (Nat.+-comm 1 (length l₁)) refl ⟩
+    (length l₁ + 1) + length l₂
+  ≡⟨ Nat.+-assoc (length l₁) 1 (length l₂) ⟩
+    length l₁ + (1 + length l₂)
+  ≡⟨⟩
+    length l₁ + length ([ a ] ++ l₂)
+  ≡˘⟨ List.length-++ l₁ ⟩
+    length (l₁ ++ [ a ] ++ l₂)
+  ∎
+    where open ≡-Reasoning
+i-nodes≡lengthl (black {l₁ = l₁} {l₂ = l₂} t₁ a t₂) =
+  begin
+    1 + (i-nodes t₁) + (i-nodes t₂)
+  ≡⟨ Eq.cong₂ _+_ (Eq.cong₂ _+_ refl (i-nodes≡lengthl t₁)) (i-nodes≡lengthl t₂) ⟩
+    1 + length l₁ + length l₂
+  ≡⟨ Eq.cong₂ _+_ (Nat.+-comm 1 (length l₁)) refl ⟩
+    (length l₁ + 1) + length l₂
+  ≡⟨ Nat.+-assoc (length l₁) 1 (length l₂) ⟩
+    length l₁ + (1 + length l₂)
+  ≡⟨⟩
+    length l₁ + length ([ a ] ++ l₂)
+  ≡˘⟨ List.length-++ l₁ ⟩
+    length (l₁ ++ [ a ] ++ l₂)
+  ∎
+    where open ≡-Reasoning
+
+i-total-height : {y : val color} {n : val nat} {l : val (list A)} → IRBT A y n l → val nat
+i-total-height leaf = 0
+i-total-height (red t₁ _ t₂) = 1 + (i-total-height t₁ Nat.⊔ i-total-height t₂)
+i-total-height (black t₁ _ t₂) = 1 + (i-total-height t₁ Nat.⊔ i-total-height t₂)
+
+i-nodes/bound/node-black-height : {y : val color} {n : val nat} {l : val (list A)} → (t : IRBT A y n l) → 1 + (i-nodes t) Nat.≥ (2 Nat.^ n)
+i-nodes/bound/node-black-height leaf = Nat.s≤s Nat.z≤n
+i-nodes/bound/node-black-height (red {n} t₁ _ t₂) =
+  let open Nat.≤-Reasoning in
+    begin
+      2 Nat.^ n
+    ≤⟨ i-nodes/bound/node-black-height t₁ ⟩
+      suc (i-nodes t₁)
+    ≤⟨ Nat.m≤m+n (suc (i-nodes t₁)) (suc (i-nodes t₂)) ⟩
+      (suc (i-nodes t₁)) + (suc (i-nodes t₂))
+    ≡⟨ Eq.cong suc (Nat.+-suc (i-nodes t₁) (i-nodes t₂)) ⟩
+      suc (suc (i-nodes t₁ + i-nodes t₂))
+    ∎
+i-nodes/bound/node-black-height (black {n} t₁ _ t₂) =
+  let open Nat.≤-Reasoning in
+    begin
+      (2 Nat.^ n) + ((2 Nat.^ n) + zero)
+    ≡⟨ Eq.sym (Eq.trans (Eq.sym (Nat.+-identityʳ ((2 Nat.^ n) + (2 Nat.^ n)))) (Nat.+-assoc ((2 Nat.^ n)) ((2 Nat.^ n)) 0)) ⟩
+      (2 Nat.^ n) + (2 Nat.^ n)
+    ≤⟨ Nat.+-monoʳ-≤ (2 Nat.^ n) (i-nodes/bound/node-black-height t₂) ⟩
+      (2 Nat.^ n) + (suc (i-nodes t₂))
+    ≤⟨ Nat.+-monoˡ-≤ ((suc (i-nodes t₂))) (i-nodes/bound/node-black-height t₁) ⟩
+      (suc (i-nodes t₁)) + (suc (i-nodes t₂))
+    ≡⟨ Eq.cong suc (Nat.+-suc (i-nodes t₁) (i-nodes t₂)) ⟩
+      suc (suc (i-nodes t₁ + i-nodes t₂))
+    ∎
+
+i-nodes/bound/log-node-black-height : {y : val color} {n : val nat} {l : val (list A)} → (t : IRBT A y n l) → n Nat.≤ ⌈log₂ (1 + (i-nodes t)) ⌉
+i-nodes/bound/log-node-black-height {A} {y} {n} t =
+  let open Nat.≤-Reasoning in
+    begin
+      n
+    ≡⟨ Eq.sym (⌈log₂2^n⌉≡n n) ⟩
+      ⌈log₂ (2 Nat.^ n) ⌉
+    ≤⟨ ⌈log₂⌉-mono-≤ (i-nodes/bound/node-black-height t) ⟩
+      ⌈log₂ (1 + (i-nodes t)) ⌉
+    ∎
+
+total-height/black-height : {y : val color} {n : val nat} {l : val (list A)} → (t : IRBT A y n l) → (i-total-height t) Nat.≤ (2 * n + 1)
+total-height/black-height leaf = Nat.z≤n
+total-height/black-height (red leaf _ leaf) = Nat.s≤s Nat.z≤n
+total-height/black-height (red (black {n} t₁₁ _ t₁₂) _ (black t₂₁ _ t₂₂)) =
+  let open Nat.≤-Reasoning in
+    begin
+      suc (suc ((i-total-height t₁₁ Nat.⊔ i-total-height t₁₂) Nat.⊔ (i-total-height t₂₁ Nat.⊔ i-total-height t₂₂)))
+    ≤⟨ Nat.s≤s (Nat.s≤s (Nat.⊔-mono-≤ (Nat.⊔-mono-≤ (total-height/black-height t₁₁) (total-height/black-height t₁₂)) (Nat.⊔-mono-≤ (total-height/black-height t₂₁) (total-height/black-height t₂₂)))) ⟩
+      suc (suc (((2 * n + 1) Nat.⊔ (2 * n + 1)) Nat.⊔ ((2 * n + 1) Nat.⊔ (2 * n + 1))))
+    ≡⟨ Eq.cong suc (Eq.cong suc (Nat.m≤n⇒m⊔n≡n Nat.≤-refl)) ⟩
+      suc (suc ((2 * n + 1) Nat.⊔ (2 * n + 1)))
+    ≡⟨ Eq.cong suc (Eq.cong suc (Nat.m≤n⇒m⊔n≡n Nat.≤-refl)) ⟩
+      suc (suc (2 * n + 1))
+    ≡⟨ Eq.cong suc (Eq.trans (Eq.cong suc (Nat.+-assoc n (n + zero) 1)) (Eq.sym (Nat.+-suc n ((n + zero) + 1)))) ⟩
+      suc (n + suc ((n + zero) + 1))
+    ≡⟨ Eq.cong suc (Eq.sym (Nat.+-assoc n (suc (n + zero)) 1)) ⟩
+      2 * (suc n) + 1
+    ∎
+total-height/black-height (black {n} t₁ _ t₂) =
+  let open Nat.≤-Reasoning in
+    begin
+      suc (i-total-height t₁ Nat.⊔ i-total-height t₂)
+    ≤⟨ Nat.s≤s (Nat.⊔-mono-≤ (total-height/black-height t₁) (total-height/black-height t₂)) ⟩
+      suc ((2 * n + 1) Nat.⊔ (2 * n + 1))
+    ≡⟨ Eq.cong suc (Nat.m≤n⇒m⊔n≡n Nat.≤-refl) ⟩
+      suc (2 * n + 1)
+    ≤⟨ Nat.s≤s (Nat.+-monoˡ-≤ 1 (Nat.+-monoʳ-≤ n (Nat.n≤1+n (n + zero)))) ⟩
+      2 * (suc n) + 1
+    ∎
+
+i-nodes/bound/total-height : {y : val color} {n : val nat} {l : val (list A)} → (t : IRBT A y n l) → (1 + (i-nodes t)) Nat.≤ (2 Nat.^ (i-total-height t))
+i-nodes/bound/total-height leaf = Nat.s≤s Nat.z≤n
+i-nodes/bound/total-height (red t₁ _ t₂) =
+  let open Nat.≤-Reasoning in
+    begin
+      suc (suc (i-nodes t₁ + i-nodes t₂))
+    ≡⟨ Eq.cong suc (Eq.sym (Nat.+-suc (i-nodes t₁) (i-nodes t₂))) ⟩
+      (suc (i-nodes t₁) + (suc (i-nodes t₂)))
+    ≤⟨ Nat.+-monoˡ-≤ (suc (i-nodes t₂)) (i-nodes/bound/total-height t₁) ⟩
+      (2 Nat.^ (i-total-height t₁)) + (suc (i-nodes t₂))
+    ≤⟨ Nat.+-monoʳ-≤ (2 Nat.^ (i-total-height t₁)) (i-nodes/bound/total-height t₂) ⟩
+      (2 Nat.^ (i-total-height t₁)) + (2 Nat.^ (i-total-height t₂))
+    ≤⟨ Nat.+-monoˡ-≤ ((2 Nat.^ (i-total-height t₂))) (Nat.^-monoʳ-≤ 2 {x = i-total-height t₁} (Nat.m≤n⇒m≤n⊔o (i-total-height t₂) (Nat.≤-refl))) ⟩
+      (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + (2 Nat.^ (i-total-height t₂))
+    ≤⟨ Nat.+-monoʳ-≤ ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))) ((Nat.^-monoʳ-≤ 2 {x = i-total-height t₂} (Nat.m≤n⇒m≤o⊔n (i-total-height t₁) (Nat.≤-refl)))) ⟩
+      (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))
+    ≡⟨ Eq.trans (Eq.sym (Nat.+-identityʳ ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))))) (Nat.+-assoc ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))) ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))) 0) ⟩
+      ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + zero))
+    ∎
+i-nodes/bound/total-height (black t₁ _ t₂) =
+  let open Nat.≤-Reasoning in
+    begin
+      suc (suc (i-nodes t₁ + i-nodes t₂))
+    ≡⟨ Eq.cong suc (Eq.sym (Nat.+-suc (i-nodes t₁) (i-nodes t₂))) ⟩
+      (suc (i-nodes t₁) + (suc (i-nodes t₂)))
+    ≤⟨ Nat.+-monoˡ-≤ (suc (i-nodes t₂)) (i-nodes/bound/total-height t₁) ⟩
+      (2 Nat.^ (i-total-height t₁)) + (suc (i-nodes t₂))
+    ≤⟨ Nat.+-monoʳ-≤ (2 Nat.^ (i-total-height t₁)) (i-nodes/bound/total-height t₂) ⟩
+      (2 Nat.^ (i-total-height t₁)) + (2 Nat.^ (i-total-height t₂))
+    ≤⟨ Nat.+-monoˡ-≤ ((2 Nat.^ (i-total-height t₂))) (Nat.^-monoʳ-≤ 2 {x = i-total-height t₁} (Nat.m≤n⇒m≤n⊔o (i-total-height t₂) (Nat.≤-refl))) ⟩
+      (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + (2 Nat.^ (i-total-height t₂))
+    ≤⟨ Nat.+-monoʳ-≤ ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))) ((Nat.^-monoʳ-≤ 2 {x = i-total-height t₂} (Nat.m≤n⇒m≤o⊔n (i-total-height t₁) (Nat.≤-refl)))) ⟩
+      (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))
+    ≡⟨ Eq.trans (Eq.sym (Nat.+-identityʳ ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + (2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))))) (Nat.+-assoc ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))) ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂))) 0) ⟩
+      ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + ((2 Nat.^ (i-total-height t₁ Nat.⊔ i-total-height t₂)) + zero))
+    ∎
+
+i-nodes/lower-bound/node-black-height : {y : val color} {n : val nat} {l : val (list A)}  → (t : IRBT A y n l) → (1 + (i-nodes t)) Nat.≤ (2 Nat.^ (2 * n + 1))
+i-nodes/lower-bound/node-black-height {A} {y} {n} t =
+  let open Nat.≤-Reasoning in
+    begin
+      1 + (i-nodes t)
+    ≤⟨ i-nodes/bound/total-height t ⟩
+      2 Nat.^ (i-total-height t)
+    ≤⟨ Nat.^-monoʳ-≤ 2 (total-height/black-height t) ⟩
+      2 Nat.^ (2 * n + 1)
+    ∎
+
+i-nodes/lower-bound/log-node-black-height : {y : val color} {n : val nat} {l : val (list A)} → (t : IRBT A y n l) → n Nat.≥ ⌊ (⌈log₂ (1 + (i-nodes t)) ⌉ ∸ 1) /2⌋
+i-nodes/lower-bound/log-node-black-height {A} {y} {n} t =
+  let open Nat.≤-Reasoning in
+    begin
+      ⌊ (⌈log₂ (1 + (i-nodes t)) ⌉ ∸ 1) /2⌋
+    ≤⟨ Nat.⌊n/2⌋-mono (h t) ⟩
+      ⌊ (2 * n) /2⌋
+    ≡⟨ Eq.sym (Eq.trans (Nat.n≡⌊n+n/2⌋ n) (Eq.cong ⌊_/2⌋ (Eq.cong₂ _+_ refl (Eq.sym (Nat.+-identityʳ n))))) ⟩
+      n
+    ∎
+    where
+      m≤o+n⇒m∸n≤o : (m n o : val nat) → (m Nat.≤ (o + n)) → ((m ∸ n) Nat.≤ o)
+      m≤o+n⇒m∸n≤o m n o m≤o+n =
+        let open Nat.≤-Reasoning in
+          begin
+            m ∸ n
+          ≤⟨ Nat.∸-monoˡ-≤ n m≤o+n ⟩
+            (o + n) ∸ n
+          ≡⟨ Nat.m+n∸n≡m o n ⟩
+            o
+          ∎
+
+      h : {y : val color} {n : val nat} {l : val (list A)} → (t : IRBT A y n l) → (⌈log₂ (1 + (i-nodes t)) ⌉ ∸ 1) Nat.≤ (2 * n)
+      h {y} {n} t = m≤o+n⇒m∸n≤o ⌈log₂ (1 + (i-nodes t)) ⌉ 1 (2 * n) (
+        let open Nat.≤-Reasoning in
+          begin
+            ⌈log₂ (1 + (i-nodes t)) ⌉
+          ≤⟨ ⌈log₂⌉-mono-≤ (i-nodes/lower-bound/node-black-height t) ⟩
+            ⌈log₂ (2 Nat.^ (2 * n + 1)) ⌉
+          ≡⟨ ⌈log₂2^n⌉≡n (2 * n + 1) ⟩
+            2 * n + 1
+          ∎)
+
+
+i-rec : {A : tp⁺} {X : tp⁻} →
+  cmp
+    ( Π (U X) λ _ →
+      Π
+        ( U
+          ( Π color λ y₁ → Π nat λ n₁ → Π (list A) λ l₁ → Π (irbt A y₁ n₁ l₁) λ _ → Π (U X) λ _ →
+            Π A λ _ →
+            Π color λ y₂ → Π nat λ n₂ → Π (list A) λ l₂ → Π (irbt A y₂ n₂ l₂) λ _ → Π (U X) λ _ →
+            X
+          )
+        ) λ _ →
+      Π color λ y → Π nat λ n → Π (list A) λ l → Π (irbt A y n l) λ _ →
+      X
+    )
+i-rec {A} {X} z f .black .zero .[] leaf = z
+i-rec {A} {X} z f .red n .(_ ++ [ a ] ++ _) (red t₁ a t₂) =
+  f
+    _ _ _ t₁ (i-rec {A} {X} z f _ _ _ t₁)
+    a
+    _ _ _ t₂ (i-rec {A} {X} z f _ _ _ t₂)
+i-rec {A} {X} z f .black .(suc _) .(_ ++ [ a ] ++ _) (black t₁ a t₂) =
+  f
+    _ _ _ t₁ (i-rec {A} {X} z f _ _ _ t₁)
+    a
+    _ _ _ t₂ (i-rec {A} {X} z f _ _ _ t₂)