changeset 953:24255e0dd027

fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 13 Sep 2024 13:25:17 +0900
parents f913c7b010b5
children 08281092430b
files BTree.agda RBTree.agda
diffstat 2 files changed, 812 insertions(+), 204 deletions(-) [+]
line wrap: on
line diff
--- a/BTree.agda	Sat Aug 24 19:20:47 2024 +0900
+++ b/BTree.agda	Fri Sep 13 13:25:17 2024 +0900
@@ -1,5 +1,4 @@
-{-# OPTIONS --cubical-compatible --allow-unsolved-metas  #-}
---  {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 module BTree where
 
--- a/RBTree.agda	Sat Aug 24 19:20:47 2024 +0900
+++ b/RBTree.agda	Fri Sep 13 13:25:17 2024 +0900
@@ -22,7 +22,7 @@
 open import logic
 open import nat
 
-open import BTree 
+open import BTree
 
 open _∧_
 
@@ -79,44 +79,80 @@
  →  (left right : bt (Color ∧ A))
  → RBtreeInvariant (node key ⟪ c , value ⟫ left right)
  → RBtreeInvariant left
-RBtreeLeftDown left right = ?
+RBtreeLeftDown {n} {A} {key} {value} {c} left right rb = lem00 _ rb refl where
+    lem00 : (tree : bt (Color ∧ A) ) → ( rb : RBtreeInvariant tree ) → tree ≡ node key ⟪ c , value ⟫ left right → RBtreeInvariant left
+    lem00 _ rb-leaf ()
+    lem00 (node key ⟪ c , value ⟫ _ _) (rb-red key value x x₁ x₂ rb rb₁) eq = subst (λ k → RBtreeInvariant k) (just-injective (cong node-left eq)) rb
+    lem00 (node key ⟪ c , value ⟫ _ _) (rb-black key value x rb rb₁) eq = subst (λ k → RBtreeInvariant k) (just-injective (cong node-left eq)) rb
 
 
 RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color}
  → (left right : bt (Color ∧ A))
  → RBtreeInvariant (node key ⟪ c , value ⟫ left right)
  → RBtreeInvariant right
-RBtreeRightDown left right = ?
+RBtreeRightDown {n} {A} {key} {value} {c} left right rb = lem00 _ rb refl where
+    lem00 : (tree : bt (Color ∧ A) ) → ( rb : RBtreeInvariant tree ) → tree ≡ node key ⟪ c , value ⟫ left right → RBtreeInvariant right
+    lem00 _ rb-leaf ()
+    lem00 (node key ⟪ c , value ⟫ _ _) (rb-red key value x x₁ x₂ rb rb₁) eq = subst (λ k → RBtreeInvariant k) (just-injective (cong node-right eq)) rb₁
+    lem00 (node key ⟪ c , value ⟫ _ _) (rb-black key value x rb rb₁) eq = subst (λ k → RBtreeInvariant k) (just-injective (cong node-right eq)) rb₁
 
 RBtreeEQ : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color}
  → {left right : bt (Color ∧ A)}
  → RBtreeInvariant (node key ⟪ c , value ⟫ left right)
  → black-depth left ≡ black-depth right
-RBtreeEQ  = ?
+RBtreeEQ {n} {A} {key} {value} {c} {left} {right} rb = lem00 _ rb refl where
+    lem00 : (tree : bt (Color ∧ A) ) → ( rb : RBtreeInvariant tree ) → tree ≡ node key ⟪ c , value ⟫ left right → black-depth left ≡ black-depth right
+    lem00 _ rb-leaf ()
+    lem00 (node key ⟪ c , value ⟫ _ _) (rb-red key value x x₁ x₂ rb rb₁) eq
+       = subst₂ (λ k l → black-depth k ≡ black-depth l) (just-injective (cong node-left eq)) (just-injective (cong node-right eq)) x₂
+    lem00 (node key ⟪ c , value ⟫ _ _) (rb-black key value x rb rb₁) eq
+       = subst₂ (λ k l → black-depth k ≡ black-depth l) (just-injective (cong node-left eq)) (just-injective (cong node-right eq)) x
 
 RBtreeToBlack : {n : Level} {A : Set n}
  → (tree : bt (Color ∧ A))
  → RBtreeInvariant tree
  → RBtreeInvariant (to-black tree)
-RBtreeToBlack = ?
+RBtreeToBlack {n} {A} tree rb = lem00 _ rb where
+    lem00 : (tree : bt (Color ∧ A) ) → ( rb : RBtreeInvariant tree ) → RBtreeInvariant (to-black tree)
+    lem00 _ rb-leaf = rb-leaf
+    lem00 (node key ⟪ c , value ⟫ left right) (rb-red key value x x₁ x₂ rb rb₁) = rb-black key value x₂ rb rb₁
+    lem00 (node key ⟪ c , value ⟫ left right) (rb-black key value x rb rb₁) = rb-black key value x rb rb₁
 
 RBtreeToBlackColor : {n : Level} {A : Set n}
  → (tree : bt (Color ∧ A))
  → RBtreeInvariant tree
  → color (to-black tree) ≡ Black
-RBtreeToBlackColor = ?
+RBtreeToBlackColor {n} {A} _ rb-leaf = refl
+RBtreeToBlackColor {n} {A} (node key ⟪ c , value ⟫ left right) (rb-red key value x x₁ x₂ rb rb₁) = refl
+RBtreeToBlackColor {n} {A} (node key ⟪ c , value ⟫ left right) (rb-black key value x rb rb₁) = refl
+
+⊥-color : ( Black ≡ Red ) → ⊥
+⊥-color ()
 
 RBtreeParentColorBlack : {n : Level} {A : Set n} → (left right  : bt (Color ∧ A)) { value : A} {key : ℕ} { c : Color}
  → RBtreeInvariant (node key ⟪ c , value ⟫ left right)
  → (color left ≡ Red) ∨ (color right ≡ Red)
  → c ≡ Black
-RBtreeParentColorBlack = ?
+RBtreeParentColorBlack {n} {A} left right {value} {key} {c} rb = lem00 _ rb refl where
+    lem00 : (tree : bt (Color ∧ A) ) → {c1 : Color } → ( rb : RBtreeInvariant tree )
+        → (node key ⟪ c1 , value ⟫ left right ≡ tree) →  (color left ≡ Red) ∨ (color right ≡ Red) → c1 ≡ Black
+    lem00 _ rb-leaf ()
+    lem00 (node key ⟪ .Red , value ⟫ _ _) (rb-red key value x x₁ x₂ rb rb₁) eq (case1 left-red)
+        = ⊥-elim (⊥-color (sym (trans (trans (sym left-red) (cong color (just-injective (cong node-left eq)))) x)))
+    lem00 (node key ⟪ .Red , value ⟫ _ _) (rb-red key value x x₁ x₂ rb rb₁) eq (case2 right-red)
+        = ⊥-elim (⊥-color (sym (trans (trans (sym right-red) (cong color (just-injective (cong node-right eq)))) x₁ )))
+    lem00 (node key ⟪ c , value ⟫ _ _) (rb-black key value x rb rb₁) eq p = cong color eq
 
 RBtreeChildrenColorBlack : {n : Level} {A : Set n} → (left right  : bt (Color ∧ A)) { value : Color ∧ A} {key : ℕ}
  → RBtreeInvariant (node key value left right)
  → proj1 value  ≡ Red
  → (color left ≡ Black) ∧  (color right ≡ Black)
-RBtreeChildrenColorBlack left right = ?
+RBtreeChildrenColorBlack {n} {A} left right {value} {key} br pv=r = lem00 _ br refl where
+    lem00 : (tree : bt (Color ∧ A) ) → ( rb : RBtreeInvariant tree ) → tree ≡ node key value left right → (color left ≡ Black) ∧  (color right ≡ Black)
+    lem00 _ rb-leaf ()
+    lem00 (node key value _ _) (rb-red key value₁ x x₁ x₂ rb rb₁) eq = ⟪ trans (sym (cong color (just-injective (cong node-left eq)))) x
+       , trans (sym (cong color (just-injective (cong node-right eq)))) x₁ ⟫
+    lem00 (node key value _ _) (rb-black key value₁ x rb rb₁) eq = ⊥-elim ( ⊥-color (sym (trans (sym pv=r) (cong proj1 (sym (just-injective (cong node-value eq)))))))
 
 --
 --  findRBT exit with replaced node
@@ -285,6 +321,7 @@
 tr>-to-black {n} {A} {key} {leaf} tr = tt
 tr>-to-black {n} {A} {key} {node key₁ value tree tree₁} tr = tr
 
+
 tr<-to-black : {n : Level} {A : Set n} {key : ℕ} {tree : bt (Color ∧ A)} → tr< key tree → tr< key (to-black tree)
 tr<-to-black {n} {A} {key} {leaf} tr = tt
 tr<-to-black {n} {A} {key} {node key₁ value tree tree₁} tr = tr
@@ -299,39 +336,53 @@
    → c ≡ Red
    → RBtreeInvariant tree
    → (black-depth tree ≡ black-depth left ) ∧ (black-depth tree ≡ black-depth right)
-red-children-eq {n} {A} = ?
-
-
-
-
-
-
-
-
-
+red-children-eq {n} {A} {_} {left} {right} {key} {value} {c} () ceq rb-leaf
+red-children-eq {n} {A} {(node key₁ ⟪ Red , value₁ ⟫ left₁ right₁)} {left} {right} {key} {value} {c} teq ceq (rb-red key₁ value₁ x x₁ x₂ rb rb₁)
+    = ⟪ begin
+          black-depth left₁ ⊔ black-depth right₁ ≡⟨ cong (λ k →   black-depth left₁ ⊔ k) (sym x₂)  ⟩
+          black-depth left₁ ⊔ black-depth left₁ ≡⟨ ⊔-idem _  ⟩
+          black-depth left₁ ≡⟨ cong black-depth (just-injective (cong node-left teq )) ⟩
+          black-depth left ∎
+    , begin
+          black-depth left₁ ⊔ black-depth right₁ ≡⟨ cong (λ k →   k ⊔ black-depth right₁) x₂  ⟩
+          black-depth right₁ ⊔ black-depth right₁ ≡⟨ ⊔-idem _  ⟩
+          black-depth right₁ ≡⟨ cong black-depth (just-injective (cong node-right teq )) ⟩
+          black-depth right ∎ ⟫
+       where open ≡-Reasoning
+red-children-eq {n} {A} {node key₁ ⟪ Black , value₁ ⟫ left₁ right₁} {left} {right} {key} {value} {c} teq ceq (rb-black key₁ value₁ x rb rb₁)
+    = ⊥-elim ( ⊥-color (trans (cong color teq) ceq))
 
 black-children-eq : {n : Level} {A : Set n}  {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color}
    → tree ≡ node key ⟪ c , value ⟫ left right
    → c ≡ Black
    → RBtreeInvariant tree
    → (black-depth tree ≡ suc (black-depth left) ) ∧ (black-depth tree ≡ suc (black-depth right))
-black-children-eq {n} {A} = ?
-
-
-
-
-
-
-
-
-
+black-children-eq {n} {A} {_} {left} {right} {key} {value} {c} () ceq rb-leaf
+black-children-eq {n} {A} {.(node key₁ ⟪ Red , value₁ ⟫ _ _)} {left} {right} {key} {value} {c} teq ceq (rb-red key₁ value₁ x x₁ x₂ rb rb₁)
+    = ⊥-elim ( ⊥-color (sym (trans (cong color teq) ceq)))
+black-children-eq {n} {A} {(node key₁ ⟪ Black , value₁ ⟫ left₁ right₁)} {left} {right} {key} {value} {c} teq ceq rb2@(rb-black key₁ value₁ x rb rb₁) =
+  ⟪ ( begin
+        suc (black-depth left₁ ⊔ black-depth right₁) ≡⟨ cong (λ k → suc (black-depth left₁ ⊔ k)) (sym (RBtreeEQ rb2)) ⟩
+        suc (black-depth left₁ ⊔ black-depth left₁) ≡⟨ cong (λ k → suc (black-depth k ⊔ black-depth k)) (just-injective (cong node-left teq )) ⟩
+        suc (black-depth left ⊔ black-depth left) ≡⟨ ⊔-idem _ ⟩
+        suc (black-depth left) ∎  ) ,  (
+     begin
+        suc (black-depth left₁ ⊔ black-depth right₁) ≡⟨ cong (λ k → suc (k ⊔ black-depth right₁)) (RBtreeEQ rb2) ⟩
+        suc (black-depth right₁ ⊔ black-depth right₁) ≡⟨ cong (λ k → suc (black-depth k ⊔ black-depth k)) (just-injective (cong node-right teq )) ⟩
+        suc (black-depth right ⊔ black-depth right) ≡⟨ ⊔-idem _ ⟩
+        suc (black-depth right) ∎ ) ⟫ where open ≡-Reasoning
 
 black-depth-cong  : {n : Level} (A : Set n)  {tree tree₁ : bt (Color ∧ A)}
    → tree ≡ tree₁ → black-depth tree ≡ black-depth tree₁
-black-depth-cong  {n} A  = ?
-
-
-
+black-depth-cong {n} A {leaf} {leaf} eq = refl
+black-depth-cong {n} A {leaf} {node _ _ _ _} ()
+black-depth-cong {n} A {node key value tree tree₂} {leaf} ()
+black-depth-cong {n} A {node key ⟪ Red , v0 ⟫ tree tree₂} {node key₁ ⟪ Red , v1 ⟫ tree₁ tree₃} eq
+    = cong₂ _⊔_ (black-depth-cong A (just-injective (cong node-left eq ))) (black-depth-cong A (just-injective (cong node-right eq )))
+black-depth-cong {n} A {node key ⟪ Red , v0 ⟫ tree tree₂} {node key₁ ⟪ Black , v1 ⟫ tree₁ tree₃} ()
+black-depth-cong {n} A {node key ⟪ Black , v0 ⟫ tree tree₂} {node key₁ ⟪ Red , v1 ⟫ tree₁ tree₃} ()
+black-depth-cong {n} A {node key ⟪ Black , v0 ⟫ tree tree₂} {node key₁ ⟪ Black , v1 ⟫ tree₁ tree₃} eq
+    = cong₂ (λ j k → suc j ⊔ suc k) (black-depth-cong A (just-injective (cong node-left eq ))) (black-depth-cong A (just-injective (cong node-right eq )))
 
 
 black-depth-resp  : {n : Level} (A : Set n)   (tree tree₁ : bt (Color ∧ A)) → {c1 c2 : Color}  { l1 l2 r1 r2 : bt (Color ∧ A)} {key1 key2 : ℕ} {value1 value2 : A}
@@ -339,40 +390,35 @@
    → color tree  ≡ color tree₁
    → black-depth l1 ≡ black-depth l2 → black-depth r1 ≡ black-depth r2
    → black-depth tree ≡ black-depth tree₁
-black-depth-resp  A _ _ = ?
-
+black-depth-resp A leaf tree₁ {c1} {c2} {l1} {l2} {r1} {r2} {key1} {key2} {value1} {value2} () eq₁ ceq bd1 bd2
+black-depth-resp A (node key value tree tree₂) leaf eq () ceq bd1 bd2
+black-depth-resp A (node key ⟪ Red , value ⟫ tree tree₂) (node key₁ ⟪ Red , value₁ ⟫ tree₁ tree₃) {c1} {c2} {l1} {l2} {r1} {r2} eq eq₁ ceq bd1 bd2 = begin
+    black-depth tree ⊔ black-depth tree₂ ≡⟨ cong₂ (λ j k → black-depth j ⊔ black-depth k) (just-injective (cong node-left eq )) (just-injective (cong node-right eq )) ⟩
+    black-depth l1 ⊔ black-depth r1 ≡⟨ cong₂ _⊔_ bd1 bd2 ⟩
+    black-depth l2 ⊔ black-depth r2 ≡⟨ cong₂ (λ j k → black-depth j ⊔ black-depth k) (just-injective (cong node-left (sym eq₁) )) (just-injective (cong node-right (sym eq₁) )) ⟩
+    black-depth tree₁ ⊔ black-depth tree₃
+    ∎ where open ≡-Reasoning
+black-depth-resp A (node key ⟪ Red , value ⟫ tree tree₂) (node key₁ ⟪ Black , value₁ ⟫ tree₁ tree₃) eq eq₁ ceq bd1 bd2 = ⊥-elim ( ⊥-color (sym ceq ))
+black-depth-resp A (node key ⟪ Black , value ⟫ tree tree₂) (node key₁ ⟪ Red , proj4 ⟫ tree₁ tree₃) eq eq₁ ceq bd1 bd2 = ⊥-elim ( ⊥-color ceq)
+black-depth-resp A (node key ⟪ Black , value ⟫ tree tree₂) (node key₁ ⟪ Black , proj4 ⟫ tree₁ tree₃) {c1} {c2} {l1} {l2} {r1} {r2} eq eq₁ ceq bd1 bd2 = begin
+    suc (black-depth tree ⊔ black-depth tree₂) ≡⟨ cong₂ (λ j k → suc (black-depth j ⊔ black-depth k)) (just-injective (cong node-left eq )) (just-injective (cong node-right eq )) ⟩
+    suc (black-depth l1 ⊔ black-depth r1) ≡⟨ cong suc ( cong₂ _⊔_ bd1 bd2) ⟩
+    suc (black-depth l2 ⊔ black-depth r2) ≡⟨ cong₂ (λ j k → suc (black-depth j ⊔ black-depth k)) (just-injective (cong node-left (sym eq₁) )) (just-injective (cong node-right (sym eq₁) )) ⟩
+    suc (black-depth tree₁ ⊔ black-depth tree₃) ∎ where open ≡-Reasoning
 
 red-children-eq1 : {n : Level} {A : Set n}  {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color}
    → tree ≡ node key ⟪ c , value ⟫ left right
    → color tree ≡ Red
    → RBtreeInvariant tree
    → (black-depth tree ≡ black-depth left ) ∧ (black-depth tree ≡ black-depth right)
-red-children-eq1 {n} {A} = ?
-
-
-
-
-
-
-
-
-
+red-children-eq1 {n} {A} {tree} {left} {right} {key} {value} {c} eq ceq rb = red-children-eq eq ((trans  (sym (cong color eq)  ) ceq )) rb
 
 black-children-eq1 : {n : Level} {A : Set n}  {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color}
    → tree ≡ node key ⟪ c , value ⟫ left right
    → color tree ≡ Black
    → RBtreeInvariant tree
    → (black-depth tree ≡ suc (black-depth left) ) ∧ (black-depth tree ≡ suc (black-depth right))
-black-children-eq1 {n} {A} = ?
-
-
-
-
-
-
-
-
-
+black-children-eq1 {n} {A} {tree} {left} {right} {key} {value} {c} eq ceq rb = black-children-eq eq ((trans  (sym (cong color eq)  ) ceq )) rb
 
 
 rbi-from-red-black : {n : Level } {A : Set n} → (n1 rp-left : bt (Color ∧ A)) → (kp : ℕ) → (vp : Color ∧ A)
@@ -400,153 +446,731 @@
 RB-repl-node {n} {A} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-left x x₁ rpl) ()
 RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-right x x₁ rpl) ()
 RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-left x x₁ rpl) ()
-RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-ll x x₁ x₂ rpl) ()
-RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-lr x x₁ x₂ x₃ rpl) ()
-RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rl x x₁ x₂ x₃ rpl) ()
-RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rr x x₁ x₂ rpl) ()
-RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) (rbr-rotate-ll x x₁ rpl) ()
-RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) (rbr-rotate-rr x x₁ rpl) ()
-RB-repl-node {n} {A} .(node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) .(node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₂) (node kg ⟪ Red , _ ⟫ t₃ _)) (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rpl) ()
-RB-repl-node {n} {A} .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ t₃ _)) (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rpl) ()
+RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-ll x x₁ x₂ x₃) ()
+RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-lr x x₁ x₂ x₃ x₄) ()
+RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rl x x₁ x₂ x₃ x₄) ()
+RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rr x₁ x₂ x₃ x₄) ()
+RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) (rbr-rotate-ll x x₁ x₂) ()
+RB-repl-node {n} {A} .(node x₂ ⟪ Black , _ ⟫ (node x₃ ⟪ Red , _ ⟫ _ _) _) .(node x₄ ⟪ Black , _ ⟫ (node x₃ ⟪ Red , _ ⟫ _ x) (node x₂ ⟪ Red , _ ⟫ x₁ _)) (rbr-rotate-lr x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) ()
+RB-repl-node {n} {A} .(node x₂ ⟪ Black , _ ⟫ _ (node x₃ ⟪ Red , _ ⟫ _ _)) .(node x₄ ⟪ Black , _ ⟫ (node x₂ ⟪ Red , _ ⟫ _ x) (node x₃ ⟪ Red , _ ⟫ x₁ _)) (rbr-rotate-rl x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) ()
+RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) (rbr-rotate-rr x x₁ x₂) ()
+
+RBTPred : {n : Level}  (A : Set n) (m : Level) → Set (n Level.⊔ Level.suc m)
+RBTPred {n} A m = (key : ℕ) → (value : A) → (before after : bt (Color ∧ A)) → replacedRBTree key value before after → Set m
+
+RBTI-induction : {n m : Level} (A : Set n) → (tree tree1 repl : bt (Color ∧ A)) → (key : ℕ) → (value : A) → tree ≡ tree1 → (rbt : replacedRBTree key value tree repl  )
+    → {P : RBTPred A m } 
+    → ( P key value leaf (node key ⟪ Red , value ⟫ leaf leaf) rbr-leaf  
+      ∧  ( (ca : Color ) → (value₂ : A) → (t t₁ : bt (Color ∧ A)) → P key value (node key ⟪ ca , value₂ ⟫ t t₁) (node key ⟪ ca , value ⟫ t t₁) rbr-node )
+      ∧  ( {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)} → (x : color t2 ≡ color t) ( x₁ : k < key ) → (rbt : replacedRBTree key value t2 t )
+         → P key value t2 t rbt → P key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t1 t) (rbr-right x x₁ rbt ) )
+      ∧  ( {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)} → (x : color t1 ≡ color t) ( x₁ : key < k ) → (rbt : replacedRBTree key value t1 t )
+         → P key value t1 t rbt 
+         → P key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t t2) (rbr-left x x₁ rbt))
+      ∧ ( {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} → (x : color t₂ ≡ Red) → (x₁ : key₁ < key)  → (rbt : replacedRBTree key value t₁ t₂ ) 
+         → P key value t₁ t₂ rbt 
+         → P key value (node key₁ ⟪ Black , value₁ ⟫ t t₁) (node key₁ ⟪ Black , value₁ ⟫ t t₂) (rbr-black-right x x₁ rbt)  )
+      ∧  ({t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} → (x : color t₂ ≡ Red ) → (x₁ : key < key₁ ) → (rbt : replacedRBTree key value t₁ t₂ )
+         → P key value t₁ t₂ rbt 
+         → P key value (node key₁ ⟪ Black , value₁ ⟫ t₁ t) (node key₁ ⟪ Black , value₁ ⟫ t₂ t) (rbr-black-left x x₁ rbt)  ) 
+      ∧ (  {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
+         → (x : color t₂ ≡ Red ) → (x₁ : color uncle ≡ Red ) → (x₂ : key < kp ) → (rbt : replacedRBTree key value t₁ t₂ )
+         →  P key value t₁ t₂ rbt
+         →  P key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t₂ t) (to-black uncle)) 
+            (rbr-flip-ll x x₁ x₂ rbt))
+      ∧ ( {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} → (x : color t₂ ≡ Red ) → (x₁ : color uncle ≡ Red ) →  (x₂ : kp < key ) → (x₃ : key < kg)   
+         → (rbt : replacedRBTree key value t₁ t₂ )
+         →  P key value t₁ t₂ rbt
+         →  P key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t t₂) (to-black uncle)) 
+           (rbr-flip-lr x x₁ x₂ x₃ rbt) )
+      ∧ ( {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
+         → (x : color t₂ ≡ Red ) → (x₁ : color uncle ≡ Red ) → (x₂ : kg < key ) → (x₃ : key < kp)  → (rbt : replacedRBTree key value t₁ t₂  )
+         → P key value t₁ t₂ rbt
+         → P key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t))
+            (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t))
+            (rbr-flip-rl x x₁ x₂ x₃ rbt)) 
+      ∧ ( {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
+         → (x : color t₂ ≡ Red ) → (x₁ : color uncle ≡ Red ) → (x₂ : kp < key )  → (rbt : replacedRBTree key value t₁ t₂  )
+         → P key value t₁ t₂ rbt
+         → P key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂))
+            (rbr-flip-rr x x₁ x₂ rbt)  ) 
+      ∧ ( {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} → (x : color t₂ ≡ Red) → (x₁ : key < kp ) → (rbt : replacedRBTree key value t₁ t₂  )
+         → P key value t₁ t₂ rbt
+         → P key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) (node kp ⟪ Black , vp ⟫ t₂ (node kg ⟪ Red , vg ⟫ t uncle)) (rbr-rotate-ll x x₁ rbt))
+      ∧ ({t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
+         → (x : color t₂ ≡ Red ) → (x₁ : kp < key ) → (rbt : replacedRBTree key value t₁ t₂ )
+         → P key value t₁ t₂ rbt
+         →  P key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂)
+            (rbr-rotate-rr x x₁ rbt)  ) 
+      ∧ ({t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A}
+         → (x : color t₃ ≡ Black) → (x₁ : kp < key )→ (x₂ : key < kg )
+         → (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃))
+         → P key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃) rbt
+         → P key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t t₂) (node kg ⟪ Red , vg ⟫ t₃ uncle))
+            (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rbt)  ) 
+      ∧ ( {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A}
+         → (x : color t₃ ≡ Black) → (x₁ : kg < key) → (x₂ : key < kp )
+         → (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃) )
+         → P key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃) rbt
+         → P key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ uncle t₂) (node kp ⟪ Red , vp ⟫ t₃ t))
+            (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rbt)  )) 
+    → P key value tree repl rbt
+RBTI-induction {n} {m} A tree leaf repl key value eq rbr-leaf {P} p = proj1 p
+RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-node {value₂} {ca} {t} {t1} ) {P} p = proj1 (proj2 p) ca value₂ t t1
+RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-right {k} {v1} {ca} {t} {t1} {t2} x x₁ rbt) {P} p 
+   = proj1 (proj2 (proj2 p)) x x₁ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p)
+RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-left x x₁ rbt) {P} p 
+   = proj1 (proj2 (proj2 (proj2 p))) x x₁ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p)
+RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-black-right x x₁ rbt) {P} p 
+   = proj1 (proj2 (proj2 (proj2 (proj2 p)))) x x₁ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p)
+RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-black-left x x₁ rbt) {P} p 
+   = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 p))))) x x₁ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p)
+RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-flip-ll {t} {t₁} {t₂} x x₁ x₂ rbt) {P} p 
+   = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p)))))) x x₁ x₂ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p) 
+RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-flip-lr x x₁ x₂ x₃ rbt) {P} p 
+   = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p))))))) x x₁ x₂ x₃ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p)
+RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-flip-rl x x₁ x₂ x₃ rbt) {P} p 
+   = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p)))))))) x x₁ x₂ x₃ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p)
+RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-flip-rr x x₁ x₂ rbt) {P} p 
+   = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p))))))))) x x₁ x₂ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p)
+RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-rotate-ll x x₁ rbt) {P} p 
+   = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p)))))))))) x x₁ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p)
+RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-rotate-rr x x₁ rbt) {P} p 
+   = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p))))))))))) x x₁ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p)
+RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rbt) {P} p 
+   = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p)))))))))))) _ _ _ _ _ x x₁ x₂ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p)
+RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rbt) {P} p 
+   = proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p)))))))))))) _ _ _ _ _ x x₁ x₂ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p)
+
 
 RB-repl→eq  : {n : Level} {A : Set n}  → (tree repl : bt (Color ∧ A)) → {key : ℕ} → {value : A}
      → RBtreeInvariant tree
      → replacedRBTree key value tree repl → black-depth tree ≡ black-depth repl
-RB-repl→eq {n} {A} = ?
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+RB-repl→eq {n} {A} tree repl {key} {value} rbt rbr = RBTI-induction A tree tree repl key value refl rbr  {λ key value b a rbt → black-depth b ≡ black-depth a } 
+     ⟪ refl , ⟪ (λ ca _ _ _ → lem00 ca _ _ _ ) , ⟪ 
+         (λ {k} {v1} {ca} {t} {t1} {t2} → lem01 {k} {v1} {ca} {t} {t1} {t2}) , ⟪ (λ {k} {v1} {ca} {t} {t1} {t2} → lem02 {k} {v1} {ca} {t} {t1} {t2}) , ⟪ 
+         (λ {t} {t₁} {t₂} {v1} → lem03 {t} {t₁} {t₂} {v1} ) , ⟪ (λ {t} {t₁} {t₂} {v₁} {k₁} → lem04 {t} {t₁} {t₂} {v₁} {k₁})  , ⟪ 
+         (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem05 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ 
+         (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem06 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ 
+         (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem07 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ 
+         (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem08 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ 
+         (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem09 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ 
+         (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem10 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ 
+         (λ {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} → lem11 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} ) , 
+         (λ {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} → lem12 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} ) ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ where
+      lem00 : (ca : Color) → ( value₂ : A) → (t t₁ : bt (Color ∧ A)) → black-depth (node key ⟪ ca , value₂ ⟫ t t₁) ≡ black-depth (node key ⟪ ca , value ⟫ t t₁)
+      lem00 Black v t t₁ = refl
+      lem00 Red v t t₁ = refl
+      lem01 : {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t2 ≡ color t) (x₁ : k < key)
+            (rbt : replacedRBTree key value t2 t) → black-depth t2 ≡ black-depth t → black-depth (node k ⟪ ca , v1 ⟫ t1 t2) ≡ black-depth (node k ⟪ ca , v1 ⟫ t1 t)
+      lem01 {k} {v1} {Red} {t} {t1} {t2} ceq x₁ rbt prev = cong ( λ k → black-depth t1 ⊔ k ) prev 
+      lem01 {k} {v1} {Black} {t} {t1} {t2} ceq x₁ rbt prev = cong ( λ k → suc (black-depth t1 ⊔ k) ) prev 
+      lem02 :  {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t1 ≡ color t) (x₁ : key < k)
+            (rbt₁ : replacedRBTree key value t1 t) → black-depth t1 ≡ black-depth t → black-depth (node k ⟪ ca , v1 ⟫ t1 t2) ≡ black-depth (node k ⟪ ca , v1 ⟫ t t2)
+      lem02 {k} {v1} {Red} {t} {t1} {t2} ceq x₁ rbt prev = cong ( λ k → k ⊔ _ ) prev
+      lem02 {k} {v1} {Black} {t} {t1} {t2} ceq x₁ rbt prev = cong ( λ k → suc (k ⊔ _) ) prev
+      lem03 :  {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} (x : color t₂ ≡ Red) (x₁ : key₁ < key) (rbt₁ : replacedRBTree key value t₁ t₂) →
+            black-depth t₁ ≡ black-depth t₂ → suc (black-depth t ⊔ black-depth t₁) ≡ suc (black-depth t ⊔ black-depth t₂) 
+      lem03 {t} x x₁ rbt eq = cong (λ k → suc (black-depth t ⊔ k)) eq
+      lem04 : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} (x : color t₂ ≡ Red) (x₁ : key < key₁) (rbt₁ : replacedRBTree key value t₁ t₂) →
+            black-depth t₁ ≡ black-depth t₂ → suc (black-depth t₁ ⊔ black-depth t) ≡ suc (black-depth t₂ ⊔ black-depth t)
+      lem04 {t} {t₁} {t₂} {v₁} x x₁ rbt eq = cong (λ k → suc (k ⊔ black-depth t)) eq
+      lem05 :  {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : key < kp) (rbt₁ : replacedRBTree key value t₁ t₂) →
+            black-depth t₁ ≡ black-depth t₂ → suc (black-depth t₁ ⊔ black-depth t ⊔ black-depth uncle) ≡ suc (black-depth t₂ ⊔ black-depth t) ⊔ black-depth (to-black uncle)
+      lem05 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ rbt eq = begin
+          suc (black-depth t₁ ⊔ black-depth t ⊔ black-depth uncle) ≡⟨ cong (λ k → suc (k ⊔ _ ⊔ _ )) eq ⟩
+          suc (black-depth t₂ ⊔ black-depth t) ⊔ suc (black-depth uncle)  ≡⟨ cong (λ k →  suc (black-depth t₂ ⊔ black-depth t) ⊔ k) (to-black-eq uncle x₁ ) ⟩
+          suc (black-depth t₂ ⊔ black-depth t) ⊔ black-depth (to-black uncle)  ∎ where open ≡-Reasoning
+      lem06 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key)
+            (x₃ : key < kg) (rbt₁ : replacedRBTree key value t₁ t₂) →
+            black-depth t₁ ≡ black-depth t₂ → suc (black-depth t ⊔ black-depth t₁ ⊔ black-depth uncle) ≡ suc (black-depth t ⊔ black-depth t₂) ⊔ black-depth (to-black uncle)
+      lem06 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ x₃ rbt eq = begin
+          suc (black-depth t ⊔ black-depth t₁ ⊔ black-depth uncle) ≡⟨ cong (λ k → suc (black-depth t ⊔ k ⊔ _ )) eq ⟩
+          suc (black-depth t ⊔ black-depth t₂) ⊔ suc (black-depth uncle)  ≡⟨ cong (λ k →  suc (black-depth t ⊔ black-depth t₂) ⊔ k) (to-black-eq uncle x₁ ) ⟩
+          suc (black-depth t ⊔ black-depth t₂) ⊔ black-depth (to-black uncle)  ∎ where open ≡-Reasoning
+      lem07 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kg < key)
+            (x₃ : key < kp) (rbt₁ : replacedRBTree key value t₁ t₂) →
+            black-depth t₁ ≡ black-depth t₂ → suc (black-depth uncle ⊔ (black-depth t₁ ⊔ black-depth t)) ≡ black-depth (to-black uncle) ⊔ suc (black-depth t₂ ⊔ black-depth t)
+      lem07 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ x₃ rbt eq = begin
+          suc (black-depth uncle ⊔ (black-depth t₁ ⊔ black-depth t)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ (k ⊔  _))) eq ⟩
+          suc (black-depth uncle ⊔ (black-depth t₂ ⊔ black-depth t)) ≡⟨ cong (λ k → k ⊔ _) (to-black-eq uncle x₁) ⟩
+          black-depth (to-black uncle) ⊔ suc (black-depth t₂ ⊔ black-depth t)  ∎ where open ≡-Reasoning
+      lem08 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) (rbt₁ : replacedRBTree key value t₁ t₂) →
+            black-depth t₁ ≡ black-depth t₂ → suc (black-depth uncle ⊔ (black-depth t ⊔ black-depth t₁)) ≡ black-depth (to-black uncle) ⊔ suc (black-depth t ⊔ black-depth t₂)
+      lem08 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ rbt eq = begin
+          suc (black-depth uncle ⊔ (black-depth t ⊔ black-depth t₁)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ (_ ⊔  k))) eq ⟩
+          suc (black-depth uncle ⊔ (black-depth t ⊔ black-depth t₂)) ≡⟨ cong (λ k → k ⊔ _) (to-black-eq uncle x₁) ⟩
+          black-depth (to-black uncle) ⊔ suc (black-depth t ⊔ black-depth t₂)  ∎ where open ≡-Reasoning
+      lem09 :  {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : key < kp) (rbt₁ : replacedRBTree key value t₁ t₂) →
+            black-depth t₁ ≡ black-depth t₂ → suc (black-depth t₁ ⊔ black-depth t ⊔ black-depth uncle) ≡ suc (black-depth t₂ ⊔ (black-depth t ⊔ black-depth uncle))
+      lem09 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ rbt eq = begin
+          suc (black-depth t₁ ⊔ black-depth t ⊔ black-depth uncle) ≡⟨ cong (λ k → suc (k ⊔ _ ⊔ _)) eq ⟩
+          suc (black-depth t₂ ⊔ black-depth t ⊔ black-depth uncle)  ≡⟨ ⊔-assoc (suc (black-depth t₂))  (suc (black-depth t)) (suc (black-depth uncle)) ⟩
+          suc (black-depth t₂ ⊔ (black-depth t ⊔ black-depth uncle))   ∎ where open ≡-Reasoning
+      lem10 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : kp < key) (rbt₁ : replacedRBTree key value t₁ t₂) →
+            black-depth t₁ ≡ black-depth t₂ → suc (black-depth uncle ⊔ (black-depth t ⊔ black-depth t₁)) ≡ suc (black-depth uncle ⊔ black-depth t ⊔ black-depth t₂)
+      lem10 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ rbt eq = begin
+          suc (black-depth uncle ⊔ (black-depth t ⊔ black-depth t₁)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ (_ ⊔ k))) eq ⟩
+          suc (black-depth uncle ⊔ (black-depth t ⊔ black-depth t₂))  ≡⟨ sym (⊔-assoc (suc (black-depth uncle))  (suc (black-depth t)) (suc (black-depth t₂))) ⟩
+          suc (black-depth uncle ⊔ black-depth t ⊔ black-depth t₂)   ∎ where open ≡-Reasoning
+      lem11 :  {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black) (x₁ : kp < key) (x₂ : key < kg)
+            (rbt₁ : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) →
+            black-depth t₁ ≡ black-depth t₂ ⊔ black-depth t₃ → suc (black-depth t ⊔ black-depth t₁ ⊔ black-depth uncle) ≡ suc
+            (black-depth t ⊔ black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth uncle))
+      lem11 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} x x₁ x₂ rbt eq = begin
+          suc (black-depth t ⊔ black-depth t₁ ⊔ black-depth uncle) ≡⟨ cong (λ k → suc (black-depth t ⊔ k ⊔ _)) eq ⟩
+          suc ((black-depth t ⊔ (black-depth t₂ ⊔ black-depth t₃ )) ⊔ black-depth uncle)  ≡⟨ cong (λ k → suc (k ⊔ black-depth uncle )) (sym ( ⊔-assoc (black-depth t) (black-depth t₂) _ )) ⟩
+          suc (((black-depth t ⊔ black-depth t₂) ⊔ black-depth t₃) ⊔ black-depth uncle)   ≡⟨ cong suc ( ⊔-assoc _ (black-depth t₃) (black-depth uncle) ) ⟩
+          suc ((black-depth t ⊔ black-depth t₂ ) ⊔ (black-depth t₃ ⊔ black-depth uncle))  ∎ where open ≡-Reasoning
+      lem12 : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black) (x₁ : kg < key) (x₂ : key < kp)
+            (rbt₁ : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) 
+            → black-depth t₁ ≡ black-depth t₂ ⊔ black-depth t₃ 
+            → suc (black-depth uncle ⊔ (black-depth t₁ ⊔ black-depth t)) ≡ suc (black-depth uncle ⊔ black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth t))
+      lem12 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} x x₁ x₂ rbt eq = begin
+          suc (black-depth uncle ⊔ (black-depth t₁ ⊔ black-depth t)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ (k ⊔ _))) eq ⟩
+          suc (black-depth uncle ⊔ ((black-depth t₂ ⊔ black-depth t₃) ⊔ black-depth t)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ k )) (( ⊔-assoc (black-depth t₂) (black-depth t₃) _ )) ⟩ 
+          suc (black-depth uncle ⊔ (black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth t)))  ≡⟨ cong suc (sym (⊔-assoc (black-depth uncle) (black-depth t₂) (black-depth t₃ ⊔ black-depth t )))  ⟩
+          suc (black-depth uncle ⊔ black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth t))  ∎ where open ≡-Reasoning
 
 
 RB-repl→ti>  : {n : Level} {A : Set n}  → (tree repl : bt (Color ∧ A)) → (key key₁ : ℕ) → (value : A)
      → replacedRBTree key value tree repl → key₁ < key → tr> key₁ tree → tr> key₁ repl
-RB-repl→ti> .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key key₁ value rbr-leaf lt tr = ⟪ lt , ⟪ tt , tt ⟫ ⟫
-RB-repl→ti> .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value (rbr-node ) lt tr = tr
-RB-repl→ti> .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-right _ x rbt) lt tr
-   = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti> _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
-RB-repl→ti> .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-left _ x rbt) lt tr
-   = ⟪ proj1 tr , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫
-RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-right x _ rbt) lt tr
-   = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti> _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
-RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-left x _ rbt) lt tr
-   = ⟪ proj1 tr , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫
-RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x _ _ rbt) lt tr
-   = ⟪ proj1 tr , ⟪ ⟪ proj1 (proj1 (proj2 tr))  , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 (proj1 (proj2 tr))))
-       , proj2 (proj2 (proj1 (proj2 tr))) ⟫ ⟫  , tr>-to-black (proj2 (proj2 tr)) ⟫ ⟫
-RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value
-   (rbr-flip-lr x _ _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫  , tr>-to-black tr5 ⟫ ⟫
-RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value
-   (rbr-flip-rl x _ _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪  RB-repl→ti> _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫   ⟫ ⟫
-RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value
-   (rbr-flip-rr x _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫   ⟫ ⟫
-RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value
-   (rbr-rotate-ll x lt2 rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5  ⟫ ⟫  = ⟪ tr4 , ⟪  RB-repl→ti> _ _ _ _ _ rbt lt tr6 , ⟪ tr3 , ⟪ tr7 , tr5 ⟫ ⟫ ⟫ ⟫
-RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key key₁ value
-   (rbr-rotate-rr x lt2 rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫  = ⟪ tr4 , ⟪ ⟪ tr3 , ⟪ tr5 , tr6 ⟫ ⟫ , RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫
-RB-repl→ti> (node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value
-   (rbr-rotate-lr left right _ _ kn _ _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5  ⟫ ⟫  = ⟪ rr00 , ⟪ ⟪ tr4 , ⟪ tr6 , proj1 (proj2 rr01) ⟫ ⟫ , ⟪ tr3 , ⟪ proj2 (proj2 rr01) , tr5 ⟫ ⟫ ⟫ ⟫ where
-       rr01 : (key₁ < kn) ∧ tr> key₁ left  ∧ tr> key₁ right
-       rr01 = RB-repl→ti> _ _ _ _ _ rbt lt tr7
-       rr00 : key₁ < kn
-       rr00 = proj1 rr01
-RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value
-   (rbr-rotate-rl left right kg kp kn _ _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫  = ⟪ rr00 , ⟪  ⟪ tr3 , ⟪ tr5 , proj1 (proj2 rr01) ⟫ ⟫ , ⟪ tr4 , ⟪ proj2 (proj2 rr01) , tr7 ⟫ ⟫ ⟫ ⟫ where
-       rr01 : (key₁ < kn) ∧ tr> key₁ left  ∧ tr> key₁ right
-       rr01 = RB-repl→ti> _ _ _ _ _ rbt lt tr6
-       rr00 : key₁ < kn
-       rr00 = proj1 rr01
+RB-repl→ti>  {n} {A} tree repl key key₁ value rbr s1 s2 = RBTI-induction A tree tree repl key value refl rbr  
+  {λ key value b a rbt → (key₁ : ℕ) → key₁ < key → tr> key₁ b  → tr> key₁ a}
+     ⟪ (λ _ x _ → ⟪ x , ⟪ tt , tt ⟫ ⟫ ) , ⟪ lem00 , ⟪ (λ {k} {v1} {ca} {t} {t1} {t2} → lem01 {k} {v1} {ca} {t} {t1} {t2} ) , ⟪ 
+        (λ {k} {v1} {ca} {t} {t1} {t2} → lem02 {k} {v1} {ca} {t} {t1} {t2} ) , ⟪ 
+        (λ {t} {t₁} {t₂} {v1} x x₁ rbt prev k3 x₃ x₂ → lem03 {t} {t₁} {t₂} {v1} x x₁ rbt prev k3 x₃ x₂ ) , ⟪ 
+        (λ {t} {t₁} {t₂} {v₁} {key₁} → lem04 {t} {t₁} {t₂} {v₁} {key₁}  ) , ⟪ 
+        (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem05 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} )  , ⟪ 
+        (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem06 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} )  , ⟪ 
+        (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem07 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}  ) , ⟪ 
+        (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem08 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ 
+        (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem09 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ) , ⟪ 
+        (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem11 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ) , ⟪ 
+        (λ {t} {t₁} {t₂} → lem12 {t} {t₁} {t₂} ) , (λ {t} {t₁} {t₂} → lem13 {t} {t₁} {t₂} ) ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ key₁ s1 s2 where
+      lem00 :  (ca : Color) (value₂ : A) (t t₁ : bt (Color ∧ A)) (key₂ : ℕ) → key₂ < key → (key₂ < key) ∧ tr> key₂ t ∧ tr> key₂ t₁ → (key₂ < key) ∧ tr> key₂ t ∧ tr> key₂ t₁
+      lem00 ca v2 t t₁ k2 x ⟪ x₁ , ⟪ x₂ , x₃ ⟫ ⟫ = ⟪ x , ⟪ x₂ , x₃  ⟫ ⟫
+      lem01 :   {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t2 ≡ color t) (x₁ : k < key)
+            (rbt : replacedRBTree key value t2 t) → ((key₂ : ℕ) → key₂ < key → tr> key₂ t2 → tr> key₂ t) → (key₂ : ℕ) → key₂ < key →
+            (key₂ < k) ∧ tr> key₂ t1 ∧ tr> key₂ t2 → (key₂ < k) ∧ tr> key₂ t1 ∧ tr> key₂ t
+      lem01 {k} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev k2 x x₂  = ⟪ proj1 x₂ , ⟪ proj1 (proj2 x₂) , prev _ x (proj2 (proj2 x₂)) ⟫ ⟫
+      lem02 : {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t1 ≡ color t) (x₁ : key < k) (rbt : replacedRBTree key value t1 t) →
+            ((key₂ : ℕ) → key₂ < key → tr> key₂ t1 → tr> key₂ t) → (key₂ : ℕ) → key₂ < key → (key₂ < k) ∧ tr> key₂ t1 ∧ tr> key₂ t2 → (key₂ < k) ∧ tr> key₂ t ∧ tr> key₂ t2
+      lem02 {k} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev k2 x x₂ = ⟪ proj1 x₂ , ⟪ prev _ x (proj1 (proj2 x₂)) , proj2 (proj2 x₂) ⟫ ⟫
+      lem03 : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ = key₂ : ℕ} (x : color t₂ ≡ Red) (x₁ : key₂ < key) (rbt : replacedRBTree key value t₁ t₂) →
+            ((key₃ : ℕ) → key₃ < key → tr> key₃ t₁ → tr> key₃ t₂) → (key₃ : ℕ) → key₃ < key → (key₃ < key₂) ∧ tr> key₃ t ∧ tr> key₃ t₁ → (key₃ < key₂) ∧ tr> key₃ t ∧ tr> key₃ t₂
+      lem03 {t} x x₁ rbt prev k3 x₃ x₂ = ⟪ proj1 x₂ , ⟪ proj1 (proj2 x₂) , prev _ x₃ (proj2 (proj2 x₂))  ⟫ ⟫
+      lem04 : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ = key₂ : ℕ} (x : color t₂ ≡ Red) (x₁ : key < key₂) (rbt : replacedRBTree key value t₁ t₂) →
+            ((key₃ : ℕ) → key₃ < key → tr> key₃ t₁ → tr> key₃ t₂) → (key₃ : ℕ) → key₃ < key → (key₃ < key₂) ∧ tr> key₃ t₁ ∧ tr> key₃ t → (key₃ < key₂) ∧ tr> key₃ t₂ ∧ tr> key₃ t
+      lem04 {t} {t₁} {t₂} {v₁} x x₁ rbt prev k3 x₃ x₂ = ⟪ proj1 x₂ , ⟪ prev _ x₃ (proj1 (proj2 x₂))  , proj2 (proj2 x₂) ⟫ ⟫
+      lem05 :  {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : key < kp) (rbt : replacedRBTree key value t₁ t₂) →
+            ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → tr> key₂ t₂) → (key₂ : ℕ) → key₂ < key →
+            (key₂ < kg) ∧ ((key₂ < kp) ∧ tr> key₂ t₁ ∧ tr> key₂ t) ∧ tr> key₂ uncle → (key₂ < kg) ∧ ((key₂ < kp) ∧ tr> key₂ t₂ ∧ tr> key₂ t) ∧ tr> key₂ (to-black uncle)
+      lem05 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ rbt prev k2 x₄ x₃ = ⟪ proj1 x₃ , 
+        ⟪ ⟪ proj1 lem10 , ⟪ prev _ x₄ (proj1 (proj2 lem10)) , proj2 (proj2 lem10)  ⟫ ⟫  , tr>-to-black (proj2 (proj2 x₃)) ⟫ ⟫ where
+          lem10 = proj1 (proj2 x₃)
+      lem06 :  {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key)
+            (x₃ : key < kg) (rbt : replacedRBTree key value t₁ t₂) → ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → tr> key₂ t₂) → (key₂ : ℕ) →
+            key₂ < key → (key₂ < kg) ∧ ((key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₁) ∧ tr> key₂ uncle →
+            (key₂ < kg) ∧ ((key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₂) ∧ tr> key₂ (to-black uncle)
+      lem06 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ x₃ rbt prev k2 x₄ x₅ = ⟪ proj1 x₅ , 
+         ⟪ ⟪ proj1 lem10 , ⟪ proj1 (proj2 lem10) , prev _ x₄ (proj2 (proj2 lem10))  ⟫ ⟫ , tr>-to-black (proj2 (proj2 x₅)) ⟫ ⟫ where
+          lem10 = proj1 (proj2  x₅)
+      lem07 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kg < key)
+            (x₃ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → tr> key₂ t₂) →
+            (key₂ : ℕ) → key₂ < key → (key₂ < kg) ∧ tr> key₂ uncle ∧ (key₂ < kp) ∧ tr> key₂ t₁ ∧ tr> key₂ t → (key₂ < kg) ∧
+            tr> key₂ (to-black uncle) ∧ (key₂ < kp) ∧ tr> key₂ t₂ ∧ tr> key₂ t
+      lem07 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ x₃ rbt prev k2 x₄ x₅ = ⟪ proj1 x₅ , ⟪ tr>-to-black (proj1 (proj2 x₅)) , 
+         ⟪ proj1 (proj2 (proj2 x₅)) , ⟪ prev _ x₄ (proj1 (proj2 (proj2 (proj2 x₅)))) , proj2 (proj2 (proj2 (proj2 x₅))) ⟫ ⟫ ⟫ ⟫
+      lem08 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key)
+            (rbt : replacedRBTree key value t₁ t₂) → ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → tr> key₂ t₂) → (key₂ : ℕ) →
+            key₂ < key → (key₂ < kg) ∧ tr> key₂ uncle ∧ (key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₁ →
+            (key₂ < kg) ∧ tr> key₂ (to-black uncle) ∧ (key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₂
+      lem08 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ rbt prev k2 x₄ x₅ = ⟪ proj1 x₅ , ⟪ tr>-to-black (proj1 (proj2 x₅)) , 
+         ⟪ proj1 (proj2 (proj2 x₅)) , ⟪ proj1 (proj2 (proj2 (proj2 x₅))) , prev _ x₄ (proj2 (proj2 (proj2 (proj2 x₅)))) ⟫ ⟫ ⟫ ⟫
+      lem09 :  {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : key < kp) (rbt : replacedRBTree key value t₁ t₂) →
+            ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → tr> key₂ t₂) → (key₂ : ℕ) → key₂ < key →
+            (key₂ < kg) ∧ ((key₂ < kp) ∧ tr> key₂ t₁ ∧ tr> key₂ t) ∧ tr> key₂ uncle → (key₂ < kp) ∧ tr> key₂ t₂ ∧ (key₂ < kg) ∧ tr> key₂ t ∧ tr> key₂ uncle
+      lem09 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ rbt prev k2 x₄ x₅ = ⟪ proj1 lem10 , 
+         ⟪ prev _ x₄ (proj1 (proj2 lem10)) , ⟪ proj1 x₅ , ⟪ proj2 (proj2 lem10) , proj2 (proj2 x₅) ⟫ ⟫ ⟫ ⟫ where
+          lem10 = proj1 (proj2 x₅)
+      lem11 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : kp < key) (rbt : replacedRBTree key value t₁ t₂) →
+            ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → tr> key₂ t₂) → (key₂ : ℕ) → key₂ < key → (key₂ < kg) ∧
+            tr> key₂ uncle ∧ (key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₁ → (key₂ < kp) ∧ ((key₂ < kg) ∧ tr> key₂ uncle ∧ tr> key₂ t) ∧ tr> key₂ t₂
+      lem11 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ rbt prev k2 x₄ x₅ = ⟪ proj1 (proj2 (proj2 x₅)) , 
+         ⟪ ⟪ proj1 x₅ , ⟪ proj1 (proj2 x₅) , proj1 (proj2 (proj2 (proj2 x₅))) ⟫ ⟫ , prev _ x₄ (proj2 (proj2 (proj2 (proj2 x₅)))) ⟫ ⟫ 
+      lem12 : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black)
+            (x₁ : kp < key) (x₂ : key < kg) (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) →
+            ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → (key₂ < kn) ∧ tr> key₂ t₂ ∧ tr> key₂ t₃) → (key₂ : ℕ) → key₂ < key →
+            (key₂ < kg) ∧ ((key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₁) ∧ tr> key₂ uncle → (key₂ < kn) ∧
+            ((key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₂) ∧ (key₂ < kg) ∧ tr> key₂ t₃ ∧ tr> key₂ uncle
+      lem12 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} x x₁ x₂ rbt prev k2 x₄ x₅ = ⟪ proj1 lem14 , ⟪ ⟪ proj1 lem15 , 
+        ⟪ proj1 (proj2 lem15) , proj1 (proj2 lem14) ⟫ ⟫ , ⟪ proj1 x₅ , ⟪ proj2 (proj2 lem14) , proj2 (proj2 x₅) ⟫ ⟫ ⟫ ⟫ where
+          lem15 = proj1 (proj2 x₅)
+          lem14 : (k2 < kn ) ∧ tr> k2 t₂ ∧ tr> k2 t₃
+          lem14 = prev _ x₄ (proj2 (proj2 lem15))
+      lem13 :  {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black) (x₁ : kg < key) (x₂ : key < kp)
+            (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) → ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → (key₂ < kn) ∧ tr> key₂ t₂ ∧ tr> key₂ t₃) →
+            (key₂ : ℕ) → key₂ < key → (key₂ < kg) ∧ tr> key₂ uncle ∧ (key₂ < kp) ∧ tr> key₂ t₁ ∧ tr> key₂ t →
+            (key₂ < kn) ∧ ((key₂ < kg) ∧ tr> key₂ uncle ∧ tr> key₂ t₂) ∧ (key₂ < kp) ∧ tr> key₂ t₃ ∧ tr> key₂ t
+      lem13 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} x x₁ x₂ rbt prev k2 x₄ x₅ = ⟪ proj1 lem14 , ⟪ ⟪ proj1 x₅ , 
+        ⟪ proj1 (proj2 x₅) , proj1 (proj2 lem14) ⟫ ⟫ , ⟪ proj1 (proj2 (proj2 x₅)) , ⟪ proj2 (proj2 lem14) , proj2 (proj2 (proj2 (proj2 x₅))) ⟫ ⟫ ⟫ ⟫ where
+          lem14 : (k2 < kn ) ∧ tr> k2 t₂ ∧ tr> k2 t₃
+          lem14 = prev _ x₄ (proj1 (proj2 (proj2 (proj2 x₅))))
+
+           
 
 RB-repl→ti<  : {n : Level} {A : Set n}  → (tree repl : bt (Color ∧ A)) → (key key₁ : ℕ) → (value : A)
      → replacedRBTree key value tree repl → key < key₁ → tr< key₁ tree → tr< key₁ repl
-RB-repl→ti< .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key key₁ value rbr-leaf lt tr = ⟪ lt , ⟪ tt , tt ⟫ ⟫
-RB-repl→ti< .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value (rbr-node ) lt tr = tr
-RB-repl→ti< .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-right _ x rbt) lt tr
-   = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti< _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
-RB-repl→ti< .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-left _ x rbt) lt tr
-   = ⟪ proj1 tr , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫
-RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-right x _ rbt) lt tr
-   = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti< _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
-RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-left x _ rbt) lt tr
-   = ⟪ proj1 tr , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫
-RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x _ _ rbt) lt tr
-   = ⟪ proj1 tr , ⟪ ⟪ proj1 (proj1 (proj2 tr))  , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 (proj1 (proj2 tr))))
-       , proj2 (proj2 (proj1 (proj2 tr))) ⟫ ⟫  , tr<-to-black (proj2 (proj2 tr)) ⟫ ⟫
-RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value
-   (rbr-flip-lr x _ _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫  , tr<-to-black tr5 ⟫ ⟫
-RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value
-   (rbr-flip-rl x _ _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪  RB-repl→ti< _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫   ⟫ ⟫
-RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value
-   (rbr-flip-rr x _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫   ⟫ ⟫
-RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value
-   (rbr-rotate-ll x lt2 rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5  ⟫ ⟫  = ⟪ tr4 , ⟪  RB-repl→ti< _ _ _ _ _ rbt lt tr6 , ⟪ tr3 , ⟪ tr7 , tr5 ⟫ ⟫ ⟫ ⟫
-RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key key₁ value
-   (rbr-rotate-rr x lt2 rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫  = ⟪ tr4 , ⟪ ⟪ tr3 , ⟪ tr5 , tr6 ⟫ ⟫ , RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫
-RB-repl→ti< (node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value
-   (rbr-rotate-lr left right _ _ kn _ _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5  ⟫ ⟫  = ⟪ rr00 , ⟪ ⟪ tr4 , ⟪ tr6 , proj1 (proj2 rr01) ⟫ ⟫ , ⟪ tr3 , ⟪ proj2 (proj2 rr01) , tr5 ⟫ ⟫ ⟫ ⟫ where
-       rr01 : (kn < key₁ ) ∧ tr< key₁ left  ∧ tr< key₁ right
-       rr01 = RB-repl→ti< _ _ _ _ _ rbt lt tr7
-       rr00 : kn < key₁
-       rr00 = proj1 rr01
-RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value
-   (rbr-rotate-rl left right kg kp kn _ _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫  = ⟪ rr00 , ⟪  ⟪ tr3 , ⟪ tr5 , proj1 (proj2 rr01) ⟫ ⟫ , ⟪ tr4 , ⟪ proj2 (proj2 rr01) , tr7 ⟫ ⟫ ⟫ ⟫ where
-       rr01 : (kn < key₁ ) ∧ tr< key₁ left  ∧ tr< key₁ right
-       rr01 = RB-repl→ti< _ _ _ _ _ rbt lt tr6
-       rr00 : kn < key₁
-       rr00 = proj1 rr01
+RB-repl→ti<  {n} {A} tree repl key key₁ value rbr s1 s2 = RBTI-induction A tree tree repl key value refl rbr  
+  {λ key value b a rbt → (key₁ : ℕ) → key < key₁ → tr< key₁ b  → tr< key₁ a}
+     ⟪ (λ _ x _ → ?  ) , ⟪ lem00 , ⟪ (λ {k} {v1} {ca} {t} {t1} {t2} → lem01 {k} {v1} {ca} {t} {t1} {t2} ) , ⟪ 
+        (λ {k} {v1} {ca} {t} {t1} {t2} → lem02 {k} {v1} {ca} {t} {t1} {t2} ) , ⟪ 
+        (λ {t} {t₁} {t₂} {v1} → lem03 {t} {t₁} {t₂} {v1} ) , ⟪ 
+        (λ {t} {t₁} {t₂} {v₁} {key₁} → lem04 {t} {t₁} {t₂} {v₁} {key₁}  ) , ⟪ 
+        (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem05 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ 
+        (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem06 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} )  , ⟪ 
+        (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem07 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}  ) , ⟪ 
+        (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem08 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ 
+        (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem09 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ) , ⟪ 
+        (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem11 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ) , ⟪ 
+        (λ {t} {t₁} {uncle} → lem12 {t} {t₁} {uncle} ) , 
+        (λ {t} {t₁} {uncle} → lem13 {t} {t₁} {uncle} ) 
+        ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ key₁ s1 s2 where
+      lem00 :  (ca : Color) (value₂ : A) (t t₁ : bt (Color ∧ A)) (key₂ : ℕ) → key < key₂ → (key < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁ → (key < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁
+      lem00 ca v2 t t₁ k2 x ⟪ x₁ , ⟪ x₂ , x₃ ⟫ ⟫ = ⟪ x , ⟪ x₂ , x₃  ⟫ ⟫
+      lem01 :   {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t2 ≡ color t) (x₁ : k < key )
+            (rbt : replacedRBTree key value t2 t) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t2 → tr< key₂ t) → (key₂ : ℕ) → key < key₂ →
+            (k < key₂ ) ∧ tr< key₂ t1 ∧ tr< key₂ t2 → (k < key₂ ) ∧ tr< key₂ t1 ∧ tr< key₂ t
+      lem01 {k} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev k2 x x₂  = ⟪ proj1 x₂ , ⟪ proj1 (proj2 x₂) , prev _ x (proj2 (proj2 x₂)) ⟫ ⟫
+      lem02 : {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t1 ≡ color t) (x₁ : key < k)
+            (rbt : replacedRBTree key value t1 t) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t1 → tr< key₂ t) →
+            (key₂ : ℕ) → key < key₂ → (k < key₂) ∧ tr< key₂ t1 ∧ tr< key₂ t2 → (k < key₂) ∧ tr< key₂ t ∧ tr< key₂ t2
+      lem02 {k} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev k2 x x₂ = ⟪ proj1 x₂ , ⟪ prev _ x (proj1 (proj2 x₂)) , proj2 (proj2 x₂) ⟫ ⟫
+      lem03 : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ = key₂ : ℕ} (x : color t₂ ≡ Red) (x₁ : key₂ < key) (rbt : replacedRBTree key value t₁ t₂) →
+            ((key₃ : ℕ) → key < key₃ → tr< key₃ t₁ → tr< key₃ t₂) → (key₃ : ℕ) → key < key₃ → (key₂ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₁ → (key₂ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₂
+      lem03 {t} x x₁ rbt prev k3 x₃ x₂ = ⟪ proj1 x₂ , ⟪ proj1 (proj2 x₂) , prev _ x₃ (proj2 (proj2 x₂))  ⟫ ⟫
+      lem04 : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} (x : color t₂ ≡ Red) (x₁ : key < key₁) (rbt : replacedRBTree key value t₁ t₂) →
+            ((key₃ : ℕ) → key < key₃ → tr< key₃ t₁ → tr< key₃ t₂) → (key₃ : ℕ) → key < key₃ → (key₁ < key₃) ∧ tr< key₃ t₁ ∧ tr< key₃ t → (key₁ < key₃) ∧ tr< key₃ t₂ ∧ tr< key₃ t
+      lem04 {t} {t₁} {t₂} {v₁} x x₁ rbt prev k3 x₃ x₂ = ⟪ proj1 x₂ , ⟪ prev _ x₃ (proj1 (proj2 x₂))  , proj2 (proj2 x₂) ⟫ ⟫
+      lem05 :  {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : key < kp) (rbt : replacedRBTree key value t₁ t₂) →
+            ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → tr< key₂ t₂) → (key₂ : ℕ) → key < key₂ → (kg < key₂) ∧
+            ((kp < key₂) ∧ tr< key₂ t₁ ∧ tr< key₂ t) ∧ tr< key₂ uncle → (kg < key₂) ∧ ((kp < key₂) ∧ tr< key₂ t₂ ∧ tr< key₂ t) ∧ tr< key₂ (to-black uncle)
+      lem05 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ rbt prev k2 x₄ x₃ = ⟪ proj1 x₃ , 
+        ⟪ ⟪ proj1 lem10 , ⟪ prev _ x₄ (proj1 (proj2 lem10)) , proj2 (proj2 lem10)  ⟫ ⟫  , tr<-to-black (proj2 (proj2 x₃)) ⟫ ⟫ where
+          lem10 = proj1 (proj2 x₃)
+      lem06 :  {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key)
+            (x₃ : key < kg) (rbt : replacedRBTree key value t₁ t₂) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → tr< key₂ t₂) → (key₂ : ℕ) → key < key₂ →
+            (kg < key₂) ∧ ((kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁) ∧ tr< key₂ uncle → (kg < key₂) ∧ ((kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₂) ∧ tr< key₂ (to-black uncle)
+      lem06 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ x₃ rbt prev k2 x₄ x₅ = ⟪ proj1 x₅ , 
+         ⟪ ⟪ proj1 lem10 , ⟪ proj1 (proj2 lem10) , prev _ x₄ (proj2 (proj2 lem10))  ⟫ ⟫ , tr<-to-black (proj2 (proj2 x₅)) ⟫ ⟫ where
+          lem10 = proj1 (proj2  x₅)
+      lem07 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kg < key)
+            (x₃ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → tr< key₂ t₂) →
+            (key₂ : ℕ) → key < key₂ → (kg < key₂) ∧ tr< key₂ uncle ∧ (kp < key₂) ∧ tr< key₂ t₁ ∧ tr< key₂ t → (kg < key₂) ∧
+            tr< key₂ (to-black uncle) ∧ (kp < key₂) ∧ tr< key₂ t₂ ∧ tr< key₂ t
+      lem07 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ x₃ rbt prev k2 x₄ x₅ = ⟪ proj1 x₅ , ⟪ tr<-to-black (proj1 (proj2 x₅)) , 
+         ⟪ proj1 (proj2 (proj2 x₅)) , ⟪ prev _ x₄ (proj1 (proj2 (proj2 (proj2 x₅)))) , proj2 (proj2 (proj2 (proj2 x₅))) ⟫ ⟫ ⟫ ⟫
+      lem08 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key)
+            (rbt : replacedRBTree key value t₁ t₂) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → tr< key₂ t₂) →
+            (key₂ : ℕ) → key < key₂ → (kg < key₂) ∧ tr< key₂ uncle ∧ (kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁ →
+            (kg < key₂) ∧ tr< key₂ (to-black uncle) ∧ (kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₂
+      lem08 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ rbt prev k2 x₄ x₅ = ⟪ proj1 x₅ , ⟪ tr<-to-black (proj1 (proj2 x₅)) , 
+         ⟪ proj1 (proj2 (proj2 x₅)) , ⟪ proj1 (proj2 (proj2 (proj2 x₅))) , prev _ x₄ (proj2 (proj2 (proj2 (proj2 x₅)))) ⟫ ⟫ ⟫ ⟫
+      lem09 :  {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : key < kp) (rbt : replacedRBTree key value t₁ t₂) →
+            ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → tr< key₂ t₂) → (key₂ : ℕ) → key < key₂ → (kg < key₂) ∧
+            ((kp < key₂) ∧ tr< key₂ t₁ ∧ tr< key₂ t) ∧ tr< key₂ uncle → (kp < key₂) ∧ tr< key₂ t₂ ∧ (kg < key₂) ∧ tr< key₂ t ∧ tr< key₂ uncle
+      lem09 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ rbt prev k2 x₄ x₅ = ⟪ proj1 lem10 , 
+         ⟪ prev _ x₄ (proj1 (proj2 lem10)) , ⟪ proj1 x₅ , ⟪ proj2 (proj2 lem10) , proj2 (proj2 x₅) ⟫ ⟫ ⟫ ⟫ where
+          lem10 = proj1 (proj2 x₅)
+      lem11 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : kp < key) (rbt : replacedRBTree key value t₁ t₂) →
+            ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → tr< key₂ t₂) → (key₂ : ℕ) → key < key₂ → (kg < key₂) ∧
+            tr< key₂ uncle ∧ (kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁ → (kp < key₂) ∧ ((kg < key₂) ∧ tr< key₂ uncle ∧ tr< key₂ t) ∧ tr< key₂ t₂
+      lem11 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ rbt prev k2 x₄ x₅ = ⟪ proj1 (proj2 (proj2 x₅)) , 
+         ⟪ ⟪ proj1 x₅ , ⟪ proj1 (proj2 x₅) , proj1 (proj2 (proj2 (proj2 x₅))) ⟫ ⟫ , prev _ x₄ (proj2 (proj2 (proj2 (proj2 x₅)))) ⟫ ⟫ 
+      lem12 : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black) (x₁ : kp < key) (x₂ : key < kg)
+            (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → (kn < key₂) ∧ tr< key₂ t₂ ∧ tr< key₂ t₃) →
+            (key₂ : ℕ) → key < key₂ → (kg < key₂) ∧ ((kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁) ∧ tr< key₂ uncle →
+            (kn < key₂) ∧ ((kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₂) ∧ (kg < key₂) ∧ tr< key₂ t₃ ∧ tr< key₂ uncle
+      lem12 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} x x₁ x₂ rbt prev k2 x₄ x₅ = ⟪ proj1 lem14 , ⟪ ⟪ proj1 lem15 , 
+        ⟪ proj1 (proj2 lem15) , proj1 (proj2 lem14) ⟫ ⟫ , ⟪ proj1 x₅ , ⟪ proj2 (proj2 lem14) , proj2 (proj2 x₅) ⟫ ⟫ ⟫ ⟫ where
+          lem15 = proj1 (proj2 x₅)
+          lem14 : (kn < k2 ) ∧ tr< k2 t₂ ∧ tr< k2 t₃
+          lem14 = prev _ x₄ (proj2 (proj2 lem15))
+      lem13 :  {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black) (x₁ : kg < key) (x₂ : key < kp)
+            (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → (kn < key₂) ∧ tr< key₂ t₂ ∧ tr< key₂ t₃) → (key₂ : ℕ) →
+            key < key₂ → (kg < key₂) ∧ tr< key₂ uncle ∧ (kp < key₂) ∧ tr< key₂ t₁ ∧ tr< key₂ t →
+            (kn < key₂) ∧ ((kg < key₂) ∧ tr< key₂ uncle ∧ tr< key₂ t₂) ∧ (kp < key₂) ∧ tr< key₂ t₃ ∧ tr< key₂ t
+      lem13 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} x x₁ x₂ rbt prev k2 x₄ x₅ = ⟪ proj1 lem14 , ⟪ ⟪ proj1 x₅ , 
+        ⟪ proj1 (proj2 x₅) , proj1 (proj2 lem14) ⟫ ⟫ , ⟪ proj1 (proj2 (proj2 x₅)) , ⟪ proj2 (proj2 lem14) , proj2 (proj2 (proj2 (proj2 x₅))) ⟫ ⟫ ⟫ ⟫ where
+          lem14 : (kn < k2 ) ∧ tr< k2 t₂ ∧ tr< k2 t₃
+          lem14 = prev _ x₄ (proj1 (proj2 (proj2 (proj2 x₅))))
+
+node-cong : {n : Level} {A : Set n} → {key key₁ : ℕ} → {value value₁ : A} → {left right left₁ right₁ : bt A} 
+       → key ≡ key₁ → value ≡ value₁ → left ≡ left₁ → right ≡ right₁ → node key value left right ≡ node key₁ value₁ left₁ right₁
+node-cong {n} {A} refl refl refl refl = refl
+
+RB-repl→ti-lem03 : {n : Level} {A : Set n} {key k : ℕ} {value v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t1 ≡ color t) (x₁ : key < k)
+    (rbt : replacedRBTree key value t1 t) → (treeInvariant t1 → treeInvariant t) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t2) → treeInvariant (node k ⟪ ca , v1 ⟫ t t2)
+RB-repl→ti-lem03 {n} {A} {key} {k} {value} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev ti = lem21 (node k ⟪ ca , v1 ⟫ t1 t2) ti refl rbt where
+  lem22 : treeInvariant t
+  lem22 = prev (treeLeftDown _ _ ti)
+  lem21 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node k ⟪ ca , v1 ⟫ t1 t2 → replacedRBTree key value t1 t  → treeInvariant (node k ⟪ ca , v1 ⟫ t t2)
+  lem21 tree ti eq rbt = ?
+
+RB-repl→ti-lem04 : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} (x : color t₂ ≡ Red) (x₁ : key₁ < key)
+    (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) 
+    → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₂)
+RB-repl→ti-lem04 = ?
+
+RB-repl→ti-lem05 : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} (x : color t₂ ≡ Red) (x₁ : key < key₁)
+    (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t₁ t) 
+     → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t₂ t)
+RB-repl→ti-lem05 = ?
+
+RB-repl→ti-lem06 : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) 
+   (x₁ : color uncle ≡ Red) (x₂ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) 
+   → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) 
+   → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t₂ t) (to-black uncle))
+RB-repl→ti-lem06 = ?
+
+RB-repl→ti-lem07 : {n : Level} {A : Set n} {key : ℕ} {value : A}  {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
+    (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) (x₃ : key < kg) (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) 
+    → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) 
+    → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t t₂) (to-black uncle))
+RB-repl→ti-lem07  = ?
+
+RB-repl→ti-lem08 : {n : Level} {A : Set n} {key : ℕ} {value : A}  → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
+     (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kg < key) (x₃ : key < kp) (rbt : replacedRBTree key value t₁ t₂) 
+     → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) 
+     → treeInvariant (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t))
+RB-repl→ti-lem08 = ?
+
+RB-repl→ti-lem09 : {n : Level} {A : Set n} {key : ℕ} {value : A}  → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
+        (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) (rbt : replacedRBTree key value t₁ t₂) →
+        (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) →
+        treeInvariant (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂))
+RB-repl→ti-lem09 = ?
+
+RB-repl→ti-lem10 : {n : Level} {A : Set n} {key : ℕ} {value : A}  → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
+        (x : color t₂ ≡ Red) (x₁ : key < kp) (rbt : replacedRBTree key value t₁ t₂) →
+        (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) →
+        treeInvariant (node kp ⟪ Black , vp ⟫ t₂ (node kg ⟪ Red , vg ⟫ t uncle))
+RB-repl→ti-lem10 = ?
+
+RB-repl→ti-lem11 : {n : Level} {A : Set n} {key : ℕ} {value : A}  → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A}
+        (x : color t₂ ≡ Red) (x₁ : kp < key) (rbt : replacedRBTree key value t₁ t₂) →
+        (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) →
+        treeInvariant (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂)
+RB-repl→ti-lem11 = ?
+
+RB-repl→ti-lem12 : {n : Level} {A : Set n} {key : ℕ} {value : A}  → {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black)
+        (x₁ : kp < key) (x₂ : key < kg) (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) →
+        (treeInvariant t₁ → treeInvariant (node kn ⟪ Red , vn ⟫ t₂ t₃)) → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) →
+        treeInvariant (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t t₂) (node kg ⟪ Red , vg ⟫ t₃ uncle))
+RB-repl→ti-lem12 = ?
+
+RB-repl→ti-lem13 : {n : Level} {A : Set n} {key : ℕ} {value : A}  → {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black)
+        (x₁ : kg < key) (x₂ : key < kp) (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) →
+        (treeInvariant t₁ → treeInvariant (node kn ⟪ Red , vn ⟫ t₂ t₃)) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) →
+        treeInvariant (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ uncle t₂) (node kp ⟪ Red , vp ⟫ t₃ t))
+RB-repl→ti-lem13 = ?
 
 RB-repl→ti : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A) ) → (key : ℕ ) → (value : A) → treeInvariant tree
        → replacedRBTree key value tree repl → treeInvariant repl
-RB-repl→ti = ?
+RB-repl→ti {n} {A} tree repl key value ti rbr = RBTI-induction A tree tree repl key value refl rbr {λ key value b a rbr → treeInvariant b → treeInvariant a }
+     ⟪ lem00 , ⟪ lem01 , ⟪ lem02 , ⟪ RB-repl→ti-lem03  , ⟪ RB-repl→ti-lem04 , ⟪ RB-repl→ti-lem05 , 
+       ⟪ RB-repl→ti-lem06 , ⟪ RB-repl→ti-lem07 , ⟪ RB-repl→ti-lem08 , ⟪ RB-repl→ti-lem09 , ⟪ RB-repl→ti-lem10 , ⟪ RB-repl→ti-lem11 
+          , ⟪ RB-repl→ti-lem12 , RB-repl→ti-lem13 ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ti where
+      lem00 : treeInvariant leaf → treeInvariant (node key ⟪ Red , value ⟫ leaf leaf)
+      lem00 ti = t-single key ⟪ Red , value ⟫
+      lem01 : (ca : Color) (value₂ : A) (t t₁ : bt (Color ∧ A)) → treeInvariant (node key ⟪ ca , value₂ ⟫ t t₁) → treeInvariant (node key ⟪ ca , value ⟫ t t₁)
+      lem01 ca v2 t t₁ ti = lem20 (node key ⟪ ca , v2 ⟫ t t₁) ti refl where
+          lem20 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node key ⟪ ca , v2 ⟫ t t₁ → treeInvariant (node key ⟪ ca , value ⟫ t t₁)
+          lem20 .leaf t-leaf ()
+          lem20 (node key v3 leaf leaf) (t-single key v3) eq = subst treeInvariant 
+             (node-cong (just-injective (cong node-key eq)) refl (just-injective (cong node-left eq)) (just-injective (cong node-right eq))) (t-single key ⟪ ca , value ⟫) 
+          lem20 (node key _ leaf (node key₁ _ _ _)) (t-right key key₁ x x₁ x₂ ti) eq = subst treeInvariant 
+             (node-cong (just-injective (cong node-key eq)) refl (just-injective (cong node-left eq)) (just-injective (cong node-right eq))) (t-right key key₁ x x₁ x₂ ti)
+          lem20 (node key₁ _ (node key _ _ _) leaf) (t-left key key₁ x x₁ x₂ ti) eq = subst treeInvariant 
+             (node-cong (just-injective (cong node-key eq)) refl (just-injective (cong node-left eq)) (just-injective (cong node-right eq))) (t-left key key₁ x x₁ x₂ ti)
+          lem20 (node key₁ _ (node key _ _ _) (node key₂ _ _ _)) (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) eq = subst treeInvariant 
+             (node-cong (just-injective (cong node-key eq)) refl (just-injective (cong node-left eq)) (just-injective (cong node-right eq))) 
+                 (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁)
+      lem02 : {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t2 ≡ color t) (x₁ : k < key)
+            (rbt : replacedRBTree key value t2 t) → (treeInvariant t2 → treeInvariant t) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t2) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t)
+      lem02 {k} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev ti = lem21 (node k ⟪ ca , v1 ⟫ t1 t2) ti refl rbt where
+          lem22 : treeInvariant t
+          lem22 = prev (treeRightDown _ _ ti)
+          lem21 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node k ⟪ ca , v1 ⟫ t1 t2 → replacedRBTree key value t2 t  → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t)
+          lem21 .leaf t-leaf ()
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) eq rbr-leaf = subst treeInvariant 
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₁ _ (subst (λ k → k < key) (sym lem23) x₁) tt tt lem22) where
+               lem23 : k₁ ≡ k
+               lem23 = just-injective (cong node-key eq)
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () rbr-node
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-right x x₁ rbt)
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-left x x₁ rbt)
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-black-right x x₁ rbt)
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-black-left x x₁ rbt)
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-ll x x₁ x₂ rbt)
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-lr x x₁ x₂ x₃ rbt)
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-rl x x₁ x₂ x₃ rbt)
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-rr x x₁ x₂ rbt)
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-ll x x₁ rbt)
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-rr x x₁ rbt)
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rbt)
+          lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rbt)
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₄ x₂ ti) eq rbr-leaf = subst treeInvariant 
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ (subst (λ k → k < key) (sym lem23) x₁) tt tt lem22) where
+               lem23 : k₃ ≡ k
+               lem23 = just-injective (cong node-key eq)
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti) eq (rbr-node {_} {_} {left} {right}) = subst treeInvariant 
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                   (t-right k₃ _ (subst (λ k → k < key) (sym lem23) x₁) (subst (λ k → tr> k₃ k) lem24 x₁₀) (subst (λ k → tr> k₃ k) lem25 x₂) lem22) where
+               lem23 : k₃ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               lem24 : t₁ ≡ left
+               lem24 = just-injective (cong node-left (just-injective (cong node-right eq)))
+               lem25 : t₂ ≡ right
+               lem25 = just-injective (cong node-right (just-injective (cong node-right eq)))
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti) eq (rbr-right {k₂} {_} {_} {t₁} {t₂} {t₃} x₃ x₄ trb) = subst treeInvariant 
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                   (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) (subst (λ k → tr> k₃ k) lem24 x₁₀) rr01 lem22) where
+               lem23 : k₃ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               lem26 : k₁ ≡ k₂
+               lem26 = just-injective (cong node-key (just-injective (cong node-right eq)))
+               lem24 : left ≡ t₂ 
+               lem24 = just-injective (cong node-left (just-injective (cong node-right eq)))
+               rr01 : tr> k₃ t₁ 
+               rr01 = RB-repl→ti> _ _ _ _ _ trb (<-trans (subst (λ k → k₃ < k ) lem26 x )  x₄ ) 
+                  (subst (λ j → tr> k₃ j) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂ )
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti) eq (rbr-left {k₂} {_} {_} {t₁} {t₂} {t₃} x₃ x₄ rbt) = subst treeInvariant 
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                   (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) rr02 rr01 lem22) where
+               lem23 : k₃ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               lem26 : k₁ ≡ k₂
+               lem26 = just-injective (cong node-key (just-injective (cong node-right eq)))
+               rr01 : tr> k₃ t₃ 
+               rr01 = subst (λ k → tr> k₃ k) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂ 
+               rr02 : tr> k₃ t₁
+               rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁)  
+                   (subst (λ j → tr> k₃ j) (just-injective (cong node-left (just-injective (cong node-right eq)))) x₁₀ )
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = subst treeInvariant 
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                   (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) rr01 rr02 lem22) where
+               lem23 : k₃ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               lem26 : k₁ ≡ k₂
+               lem26 = just-injective (cong node-key (just-injective (cong node-right eq)))
+               rr01 : tr> k₃ t₁ 
+               rr01 = subst (λ k → tr> k₃ k) (just-injective (cong node-left (just-injective (cong node-right eq))))  x₁₀
+               rr02 : tr> k₃ t₃
+               rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁)  
+                  (subst (λ k → tr> k₃ k) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂ )
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = subst treeInvariant 
+              (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) rr02 rr01 lem22) where
+               lem23 : k₃ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               lem26 : k₁ ≡ k₂
+               lem26 = just-injective (cong node-key (just-injective (cong node-right eq)))
+               rr01 : tr> k₃ t₁ 
+               rr01 = subst (λ k → tr> k₃ k) (just-injective (cong node-right (just-injective (cong node-right eq))))  x₂
+               rr02 : tr> k₃ t₃
+               rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁)  
+                  (subst (λ k → tr> k₃ k) (just-injective (cong node-left (just-injective (cong node-right eq)))) x₁₀ )
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti) eq (rbr-flip-ll x₃ x₄ x₅ rbt) = ⊥-elim ( ⊥-color ceq )
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti) eq (rbr-flip-lr x₃ x₄ x₅ x₆ rbt) = ⊥-elim ( ⊥-color ceq )
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti) eq (rbr-flip-rl x₃ x₄ x₅ x₆ rbt) = ⊥-elim ( ⊥-color ceq )
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti) eq (rbr-flip-rr x₃ x₄ x₅ rbt) = ⊥-elim ( ⊥-color ceq )
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) 
+           = subst treeInvariant 
+              (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr02 rr01 lem22) where
+               lem23 : k₃ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               lem27 : k₃ < kp
+               lem27 = subst (λ k → k < kp) (sym lem23) (<-trans x₁ x₄)
+               rr04 : (k₃ < kg) ∧ ((k₃ < kp) ∧ tr> k₃ t₁ ∧ tr> k₃ t) ∧ tr> k₃ uncle
+               rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+               rr01 : (k₃ < kg) ∧ tr> k₃ t ∧ tr> k₃ uncle
+               rr01 = ⟪ proj1 rr04 , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫
+               rr02 : tr> k₃ t₂
+               rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj1 (proj2 rr04))))
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) 
+           = subst treeInvariant 
+              (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr01 rr02 lem22) where
+               lem23 : k₃ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               rr04 : (k₃ < kg) ∧ tr> k₃ uncle ∧ ((k₃ < kp) ∧ tr> k₃ t ∧ tr> k₃ t₁) 
+               rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+               lem27 : k₃ < kp
+               lem27 = proj1 (proj2 (proj2 rr04))
+               rr01 : (k₃ < kg) ∧ tr> k₃ uncle ∧ tr> k₃ t
+               rr01 = ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫
+               rr02 : tr> k₃ t₂
+               rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj2 (proj2 rr04))))
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) 
+           = subst treeInvariant 
+              (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr05 rr06 lem22) where
+               lem23 : k₃ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               rr04 : (k₃ < kg) ∧ ((k₃ < kp) ∧ tr> k₃ t ∧ tr> k₃ t₁) ∧ tr> k₃ uncle 
+               rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+               rr01 : (k₃ < kn) ∧ tr> k₃ t₂ ∧ tr> k₃ t₃
+               rr01 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj1 (proj2 rr04)))) 
+               lem27 : k₃ < kn
+               lem27 = proj1 rr01
+               rr05 : (k₃ < kp) ∧ tr> k₃ t ∧ tr> k₃ t₂
+               rr05 = ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr01) ⟫ ⟫
+               rr06 : (k₃ < kg) ∧ tr> k₃ t₃ ∧ tr> k₃ uncle 
+               rr06 = ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr01) , proj2 (proj2 rr04) ⟫ ⟫
+          lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) 
+           = subst treeInvariant 
+              (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr05 rr06 lem22) where
+               lem23 : k₃ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               rr04 : (k₃ < kg) ∧ tr> k₃ uncle ∧ ( (k₃ < kp) ∧ tr> k₃ t₁ ∧ tr> k₃ t)
+               rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+               rr01 : (k₃ < kn) ∧ tr> k₃ t₂ ∧ tr> k₃ t₃
+               rr01 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj2 (proj2 rr04))) ) 
+               lem27 : k₃ < kn
+               lem27 = proj1 rr01
+               rr05 : (k₃ < kg) ∧ tr> k₃ uncle ∧ tr> k₃ t₂
+               rr05 = ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr01) ⟫ ⟫
+               rr06 : (k₃ < kp) ∧ tr> k₃ t₃ ∧ tr> k₃ t
+               rr06 = ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr01) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti₁) eq rbr-leaf = subst treeInvariant
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                 (t-node _ _ _ x (subst (λ j → j < key) (sym lem23) x₁) x₁₀ x₂ tt tt ti₁ (t-single key ⟪ Red , value ⟫)) where
+               lem23 : k₃ ≡ k
+               lem23 = just-injective (cong node-key eq)
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () rbr-node
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-right x₃ x₄ rbt)
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-left x₃ x₄ rbt)
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-black-right x₃ x₄ rbt)
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-black-left x₃ x₄ rbt)
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-ll x₃ x₄ x₅ rbt)
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-lr x₃ x₄ x₅ x₆ rbt)
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-rl x₃ x₄ x₅ x₆ rbt)
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-rr x₃ x₄ x₅ rbt)
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-ll x₃ x₄ rbt)
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-rr x₃ x₄ rbt) 
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-lr t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) 
+          lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-rl t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) 
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) () rbr-leaf
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ {_} {_} {_} {t} {t₁} {t₂} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-node {_} {_} {t₃} {t₄}) 
+            = subst treeInvariant
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                 (t-node _ _ _ x (subst (λ j → j < key) (sym lem23) x₁) x₂ x₃ (proj1 (proj2 rr04))  (proj2 (proj2 rr04)) ti₁ lem22) where
+               lem23 : k₁ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               rr04 : (k₁ < key) ∧ tr> k₁ t₃ ∧ tr> k₁ t₄
+               rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-right {k₃} {_} {_} {t₁} {t₂} {t₃} x₆ x₇ rbt) 
+            = subst treeInvariant
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                 (t-node _ _ _ x (proj1 rr04) x₂ x₃ (proj1 (proj2 rr04)) rr05 ti₁ lem22) where
+               lem23 : k₁ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               rr04 : (k₁ < k₃) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃
+               rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+               rr05 : tr> k₁ t₁
+               rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁)  (proj2 (proj2 rr04))
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-left {k₃} {_} {_} {t₁} {t₂} {t₃}  x₆ x₇ rbt) 
+            = subst treeInvariant
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                 (t-node _ _ _ x (proj1 rr04) x₂ x₃ rr05 (proj2 (proj2 rr04)) ti₁ lem22) where
+               lem23 : k₁ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               rr04 : (k₁ < k₃) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃
+               rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
+               rr05 : tr> k₁ t₁
+               rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁)  (proj1 (proj2 rr04))
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₃} x₆ x₇ rbt) 
+            = subst treeInvariant
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                 (t-node _ _ _ x (proj1 rr04) x₂ x₃ (proj1 (proj2 rr04)) rr05 ti₁ lem22) where
+               lem23 : k₁ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               rr04 : (k₁ < k₃) ∧ tr> k₁ t₁ ∧ tr> k₁ t₂
+               rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
+               rr05 : tr> k₁ t₃
+               rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 rr04)) 
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₃} x₆ x₇ rbt) 
+           = subst treeInvariant
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                 (t-node _ _ _ x (proj1 rr04) x₂ x₃ rr05 (proj2 (proj2 rr04)) ti₁ lem22) where
+               lem23 : k₁ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               rr04 : (k₁ < k₃) ∧ tr> k₁ t₂ ∧ tr> k₁ t₁
+               rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
+               rr05 : tr> k₁ t₃
+               rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 rr04)) 
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) eq (rbr-flip-ll x₆ x₇ x₈ rbt) = ⊥-elim ( ⊥-color ceq )
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) eq (rbr-flip-lr x₆ x₇ x₈ x₉ rbt) = ⊥-elim ( ⊥-color ceq )
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) eq (rbr-flip-rl x₆ x₇ x₈ x₉ rbt) = ⊥-elim ( ⊥-color ceq )
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) eq (rbr-flip-rr x₆ x₇ x₈ rbt) = ⊥-elim ( ⊥-color ceq )
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} x₆ x₇ rbt) 
+           = subst treeInvariant
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                 (t-node _ _ _ x (proj1 (proj1 (proj2 rr04))) x₂ x₃ rr05 ⟪ proj1 rr04 , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫  ti₁ lem22) where
+               lem23 : k₁ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               rr04 : (k₁ < kg) ∧ ((k₁ < kp) ∧ tr> k₁ t₂ ∧ tr> k₁ t₁) ∧ tr> k₁ uncle
+               rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
+               rr05 : tr> k₁ t₃
+               rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj1 (proj2 rr04))))
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} x₆ x₇ rbt) 
+           = subst treeInvariant
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                 (t-node _ _ _ x (proj1 (proj2 (proj2 rr04))) x₂ x₃  ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ rr05 ti₁ lem22) where
+               lem23 : k₁ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               rr04 : (k₁ < kg) ∧ tr> k₁ uncle ∧ ((k₁ < kp) ∧ tr> k₁ t₁ ∧ tr> k₁ t₂) 
+               rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
+               rr05 : tr> k₁ t₃
+               rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj2 (proj2 rr04))))
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) 
+           = subst treeInvariant
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                 (t-node _ _ _ x (proj1 rr05) x₂ x₃ ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr05) ⟫ ⟫  
+                    ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr05) , proj2 (proj2 rr04) ⟫ ⟫  ti₁ lem22) where
+               lem23 : k₁ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               rr04 : (k₁ < kg) ∧ ((k₁ < kp) ∧ tr> k₁ t ∧ tr> k₁ t₁) ∧ tr> k₁ uncle 
+               rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
+               rr05 : (k₁ < kn) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃
+               rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj1 (proj2 rr04)))) 
+          lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) 
+           = subst treeInvariant
+             (node-cong lem23 refl (just-injective (cong node-left eq)) refl) 
+                 (t-node _ _ _ x (proj1 rr05) x₂ x₃ ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr05) ⟫ ⟫  
+                    ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr05) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫  ti₁ lem22) where
+               lem23 : k₁ ≡ k
+               lem23 = just-injective (cong node-key eq)
+               rr04 : (k₁ < kg) ∧ tr> k₁ uncle ∧ ((k₁ < kp) ∧ tr> k₁ t₁ ∧ tr> k₁ t)   
+               rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti ))
+               rr05 : (k₁ < kn) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃
+               rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj2 (proj2 rr04)))) 
+
+PGtoRBinvariant1 : {n : Level} {A : Set n}
+           → (tree orig : bt (Color ∧ A) )
+           → {key : ℕ }
+           →  (rb : RBtreeInvariant orig)
+           →  (stack : List (bt (Color ∧ A)))  → (si : stackInvariant key tree orig stack )
+           →  RBtreeInvariant tree
+PGtoRBinvariant1 tree .tree rb .(tree ∷ []) s-nil = rb
+PGtoRBinvariant1 tree orig rb = {!!}
+
+RBI-child-replaced : {n : Level} {A : Set n} (tr : bt (Color ∧ A)) (key : ℕ) →  RBtreeInvariant tr → RBtreeInvariant (child-replaced key tr)
+RBI-child-replaced {n} {A} leaf key rbi = rbi
+RBI-child-replaced {n} {A} (node key₁ value tr tr₁) key rbi with <-cmp key key₁
+... | tri< a ¬b ¬c = RBtreeLeftDown _ _ rbi
+... | tri≈ ¬a b ¬c = rbi
+... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi
+
 
 --
 -- if we consider tree invariant, this may be much simpler and faster
@@ -571,21 +1195,6 @@
 ... | s2-1s2p _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫
 
 
-PGtoRBinvariant1 : {n : Level} {A : Set n}
-           → (tree orig : bt (Color ∧ A) )
-           → {key : ℕ }
-           →  (rb : RBtreeInvariant orig)
-           →  (stack : List (bt (Color ∧ A)))  → (si : stackInvariant key tree orig stack )
-           →  RBtreeInvariant tree
-PGtoRBinvariant1 tree .tree rb .(tree ∷ []) s-nil = rb
-PGtoRBinvariant1 tree orig rb = ?
-
-RBI-child-replaced : {n : Level} {A : Set n} (tr : bt (Color ∧ A)) (key : ℕ) →  RBtreeInvariant tr → RBtreeInvariant (child-replaced key tr)
-RBI-child-replaced {n} {A} leaf key rbi = rbi
-RBI-child-replaced {n} {A} (node key₁ value tr tr₁) key rbi with <-cmp key key₁
-... | tri< a ¬b ¬c = RBtreeLeftDown _ _ rbi
-... | tri≈ ¬a b ¬c = rbi
-... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi
 
 --
 -- create RBT invariant after findRBT, continue to replaceRBT