--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/RBTree1.agda	Sun Oct 06 17:59:51 2024 +0900
@@ -0,0 +1,1361 @@
+-- {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS  --allow-unsolved-metas --cubical-compatible  #-}
+module RBTree1 where
+
+open import Level hiding (suc ; zero ; _⊔_ )
+
+open import Data.Nat hiding (compare)
+open import Data.Nat.Properties as NatProp
+open import Data.Maybe
+open import Data.Maybe.Properties
+open import Data.Empty
+open import Data.Unit
+open import Data.List
+open import Data.List.Properties
+open import Data.Product
+
+open import Function as F hiding (const)
+
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+open import logic
+open import nat
+
+open import BTree
+open import RBTreeBase
+
+open _∧_
+
+
+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 .leaf t-leaf () rbt
+  lem21 .(node k₃ value₁ leaf leaf) (t-single k₃ value₁) eq rbr-leaf = subst treeInvariant 
+     (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left key k₃ (subst (λ k → key < k) (sym lem23) x₁) tt tt lem22) where
+       lem23 : k₃ ≡ k
+       lem23 = just-injective (cong node-key eq)
+  lem21 .(node key value leaf leaf) (t-single key value) () rbr-node
+  lem21 .(node key value leaf leaf) (t-single key value) () (rbr-right x x₁ rbt)
+  lem21 .(node key value leaf leaf) (t-single key value) () (rbr-left x x₁ rbt)
+  lem21 .(node key value leaf leaf) (t-single key value) () (rbr-black-right x x₁ rbt)
+  lem21 .(node key value leaf leaf) (t-single key value) () (rbr-black-left x x₁ rbt) 
+  lem21 .(node key value leaf leaf) (t-single key value) () (rbr-flip-ll x x₁ x₂ rbt) 
+  lem21 .(node key value leaf leaf) (t-single key value) () (rbr-flip-lr x x₁ x₂ x₃ rbt) 
+  lem21 .(node key value leaf leaf) (t-single key value) () (rbr-flip-rl x x₁ x₂ x₃ rbt) 
+  lem21 .(node key value leaf leaf) (t-single key value) () (rbr-flip-rr x x₁ x₂ rbt) 
+  lem21 .(node key value leaf leaf) (t-single key value) () (rbr-rotate-ll x x₁ rbt) 
+  lem21 .(node key value leaf leaf) (t-single key value) () (rbr-rotate-rr x x₁ rbt) 
+  lem21 .(node key value leaf leaf) (t-single key value) () (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rbt) 
+  lem21 .(node key value leaf leaf) (t-single key value) () (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 refl (just-injective (cong node-right eq))) (t-node _ _ k₃ (subst (λ j → key < j) (sym lem23) x₁)  x tt tt x₁₀ x₂ (t-single _ _) ti₁ ) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq )
+  lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () rbr-node 
+  lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-right x₃ x₄ rbt) 
+  lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-left x₃ x₄ rbt) 
+  lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-black-right x₃ x₄ rbt) 
+  lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-black-left x₃ x₄ rbt) 
+  lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-ll x₃ x₄ x₅ rbt) 
+  lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-lr x₃ x₄ x₅ x₆ rbt) 
+  lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-rl x₃ x₄ x₅ x₆ rbt) 
+  lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-rr x₃ x₄ x₅ rbt) 
+  lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-rotate-ll x₃ x₄ rbt) 
+  lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-rotate-rr x₃ x₄ rbt) 
+  lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-rotate-lr t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) 
+  lem21 .(node k₄ _ leaf (node key₁ _ _ _)) (t-right k₄ key₁ x x₁₀ x₂ ti₁) () (rbr-rotate-rl t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) 
+  lem21 (node k₄ _ (node k₃ _ t₁ t₂) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-node {_} {_} {t₃} {t₄} ) =  subst treeInvariant 
+     (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left key k₄ (proj1 rr04) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) lem22 ) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq )
+       rr04 : (key < k₄) ∧ tr< k₄ t₃ ∧ tr< k₄ t₄
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+  lem21 (node k₄ _ (node k₃ _ t₁ t₂) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₁₁ x₃ rbt) = subst treeInvariant 
+     (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22 ) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq )
+       rr04 : (k₁ < k₄) ∧ tr< k₄ t₄ ∧ tr< k₄ t₅
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁)  (proj2 (proj2 rr04))
+  lem21 (node k₄ _ (node k₃ _ t₁ t₂) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₁₁ x₃ rbt) = subst treeInvariant 
+     (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22 ) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq )
+       rr04 : (k₁ < k₄) ∧ tr< k₄ t₄ ∧ tr< k₄ t₅
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁)  (proj1 (proj2 rr04))
+  lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂}  x₁₁ x₃ rbt) = subst treeInvariant 
+     (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22 ) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq )
+       rr04 : (k₂ < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t₂   
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁)  (proj2 (proj2 rr04))
+  lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂}  x₁₁ x₃ rbt) = subst treeInvariant 
+     (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22 ) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq )
+       rr04 : (k₂ < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₁  
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁)  (proj1 (proj2 rr04))
+  lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-flip-ll x₁₁ x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-flip-lr x₁₁ x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-flip-rl x₁₁ x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-flip-rr x₁₁ x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left k₃ k₄ x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} x₁₁ x₃ rbt) = subst treeInvariant 
+     (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 (proj1 (proj2 rr04))) rr02 
+           ⟪ proj1 rr04  , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫  lem22 ) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq )
+       rr04 : (kg < k₄) ∧ ((kp < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₁ ) ∧ tr< k₄ uncle
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁)  (proj1 (proj2 (proj1 (proj2 rr04))))
+  lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left 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 refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 (proj2 (proj2 rr04))) 
+           ⟪ proj1 rr04  , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫  rr02  lem22 ) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq )
+       rr04 : (kg < k₄) ∧ tr< k₄ uncle ∧ ((kp < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t₂)
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁)  (proj2 (proj2 (proj2 (proj2 rr04))))
+  lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left 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 refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr02) 
+   ⟪ proj1 (proj1 (proj2 rr04))  , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr02) ⟫ ⟫  ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr02) , proj2 (proj2 rr04) ⟫ ⟫  lem22 ) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq )
+       rr04 : (kg < k₄) ∧ ((kp < k₄) ∧ tr< k₄ t ∧ tr< k₄ t₁) ∧ tr< k₄ uncle 
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : (kn < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁)  (proj2 (proj2 (proj1 (proj2 rr04))))
+  lem21 .(node k₄ _ (node k₃ _ _ _) leaf) (t-left 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 refl (just-injective (cong node-right eq))) (t-left _ k₄ (proj1 rr02) 
+   ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr02) ⟫ ⟫  ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr02) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫  lem22 ) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq )
+       rr04 : (kg < k₄) ∧ tr< k₄ uncle ∧ ((kp < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t) 
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : (kn < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁)  (proj1 (proj2 (proj2 (proj2 rr04))))
+  lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-node  {_} {_} {t₃} {t₄}) = subst treeInvariant
+     (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) x₁₀ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) x₄ x₅ lem22 ti₂) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq)
+       rr04 : (key < k₄) ∧ tr< k₄ t₃ ∧ tr< k₄ t₄
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+  lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-right  {k₁} {_} {_} {t₃} {t₄} {t₅} x₁₁ x₆ rbt) = subst treeInvariant
+     (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) x₁₀ (proj1 (proj2 rr04)) rr02 x₄ x₅ lem22 ti₂) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq)
+       rr04 : (k₁ < k₄) ∧ tr< k₄ t₄ ∧ tr< k₄ t₅
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁)  (proj2 (proj2 rr04))
+  lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-left  {k₁} {_} {_} {t₃} {t₄} {t₅} x₁₁ x₆ rbt) = subst treeInvariant
+     (node-cong lem23 refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) x₁₀ rr02 (proj2 (proj2 rr04)) x₄ x₅ lem22 ti₂) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq)
+       rr04 : (k₁ < k₄) ∧ tr< k₄ t₄ ∧ tr< k₄ t₅
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁)  (proj1 (proj2 rr04))
+  lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ 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 refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) x₁₀ (proj1 (proj2 rr04)) rr02 x₄ x₅ lem22 ti₂) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq)
+       rr04 : (k₂ < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t₂
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁)  (proj2 (proj2 rr04))
+  lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ 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 refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) x₁₀  rr02 (proj2 (proj2 rr04)) x₄ x₅ lem22 ti₂) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq)
+       rr04 : (k₂ < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₁
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁)  (proj1 (proj2 rr04))
+  lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ 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 key₂ _ _ _)) (t-node k₃ k₄ key₂ 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 key₂ _ _ _)) (t-node k₃ k₄ key₂ 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 key₂ _ _ _)) (t-node k₃ k₄ key₂ 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 key₂ _ _ _)) (t-node k₃ k₄ key₂ 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 refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 (proj1 (proj2 rr04))) x₁₀  rr02 
+          ⟪ proj1 rr04 , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫  x₄ x₅ lem22 ti₂) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq)
+       rr04 : (kg < k₄) ∧ ((kp < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₁) ∧ tr< k₄ uncle 
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2  (proj1 (proj2 rr04))))
+  lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ 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 refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 (proj2 (proj2 rr04))) x₁₀  
+          ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫  rr02 x₄ x₅ lem22 ti₂) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq)
+       rr04 : (kg < k₄) ∧ tr< k₄ uncle ∧ ((kp < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t₂)
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2  (proj2 (proj2 rr04))))
+  lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ 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 refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr02) x₁₀  
+          ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr02) ⟫ ⟫  ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr02) , proj2 (proj2 rr04) ⟫ ⟫  
+             x₄ x₅ lem22 ti₂) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq)
+       rr04 : (kg < k₄) ∧ ((kp < k₄) ∧ tr< k₄ t ∧ tr< k₄ t₁) ∧ tr< k₄ uncle
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : (kn < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj2 (proj2  (proj1 (proj2 rr04))))
+  lem21 .(node k₄ _ (node k₃ _ _ _) (node key₂ _ _ _)) (t-node k₃ k₄ key₂ 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 refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr02) x₁₀  
+          ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr02) ⟫ ⟫  ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr02) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫  
+             x₄ x₅ lem22 ti₂) where
+       lem23 : k₄ ≡ k
+       lem23 = just-injective (cong node-key eq)
+       rr04 : (kg < k₄) ∧ tr< k₄ uncle ∧ ((kp < k₄) ∧ tr< k₄ t₁ ∧ tr< k₄ t) 
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti))
+       rr02 : (kn < k₄) ∧ tr< k₄ t₂ ∧ tr< k₄ t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt (subst (λ j → key < j) (sym lem23) x₁) (proj1 (proj2  (proj2 (proj2 rr04))))
+
+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 {n} {A} {key} {value} {t} {t1} {t2} {v1} {k} ceq x₁ rbt prev ti = lem21 (node k ⟪ Black , v1 ⟫ t t1) ti refl rbt where 
+  lem22 : treeInvariant t2
+  lem22 = prev (treeRightDown _ _ ti)
+  lem21 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node k ⟪ Black , v1 ⟫ t t1 → replacedRBTree key value t1 t2  → treeInvariant (node k ⟪ Black , v1 ⟫ t t2)
+  lem21 _ t-leaf () rbt
+  lem21 _ (t-single key value) eq rbr-leaf = subst treeInvariant (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ x₁ _ _ lem22) 
+  lem21 _ (t-single key value) () (rbr-node {_} {_} {t₃} {t₄})
+  lem21 _ (t-single key value) () (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt)
+  lem21 _ (t-single key value) () (rbr-left  {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) 
+  lem21 _ (t-single key value) () (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) 
+  lem21 _ (t-single key value) () (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) 
+  lem21 _ (t-single key value) () (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) 
+  lem21 _ (t-single key value) () (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) 
+  lem21 _ (t-single key value) () (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) 
+  lem21 _ (t-single key value) () (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) 
+  lem21 _ (t-single key value) () (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) 
+  lem21 _ (t-single key value) () (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) 
+  lem21 _ (t-single key value) () (rbr-rotate-rl  {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) 
+  lem21 _ (t-single key value) () (rbr-rotate-lr {t} {t₁} {uncle}  t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) 
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) () rbr-leaf
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant 
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ x₁ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) lem22) where
+       rr04 : (k < _ ) ∧ tr> k t₃ ∧ tr> k t₄
+       rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) = subst treeInvariant 
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22) where
+       rr04 : (k < k₁ ) ∧ tr> k t₄ ∧ tr> k t₅
+       rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr> k t₃
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04)) 
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) = subst treeInvariant 
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22) where
+       rr04 : (k < k₁) ∧ tr> k t₄ ∧ tr> k t₅
+       rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr> k t₃
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04)) 
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22) where
+       rr04 : (k < k₂) ∧ tr> k t₁ ∧ tr> k t₂
+       rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr> k t₃
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04)) 
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22) where
+       rr04 : (k < k₂) ∧ tr> k t₂ ∧ tr> k t₁
+       rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr> k t₃
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04)) 
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) 
+          ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫  (tr>-to-black (proj2 (proj2 rr04))) lem22) where
+       rr04 : (k < kg) ∧ ((k < kp) ∧ tr> k t₂ ∧ tr> k t₁) ∧ tr> k uncle
+       rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr> k t₃
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr04))) ) 
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) 
+          ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , rr02 ⟫ ⟫  (tr>-to-black (proj2 (proj2 rr04))) lem22) where
+       rr04 : (k < kg) ∧ ((k < kp) ∧ tr> k t₁ ∧ tr> k t₂) ∧ tr> k uncle
+       rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr> k t₃
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr04)))) 
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) 
+           (tr>-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫  lem22) where
+       rr04 : (k < kg) ∧ tr> k uncle ∧ ((k < kp) ∧ tr> k t₂ ∧ tr> k t₁)
+       rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr> k t₃
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr04))) ) 
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-right _ _ (proj1 rr04) 
+           (tr>-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj1 (proj2 (proj2 (proj2 rr04))) , rr02 ⟫ ⟫  lem22) where
+       rr04 : (k < kg) ∧ tr> k uncle ∧ ((k < kp) ∧ tr> k t₁ ∧ tr> k t₂)
+       rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr> k t₃
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr04))) ) 
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄  rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄  rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t} {t₁} x x₁₀ x₂ ti₁) eq rbr-leaf = subst treeInvariant (node-cong refl refl (just-injective (cong node-left eq)) refl) 
+     (t-node _ _ _ (subst (λ j → key₂ < j ) lem23 x) x₁ (subst (λ k → tr< k t) lem23 x₁₀) (subst (λ k → tr< k t₁) lem23 x₂) tt tt ti₁ lem22) where
+       lem23 : key₁ ≡ k
+       lem23 = just-injective (cong node-key eq) 
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₂ < j ) lem23 x) x₁ 
+          (subst (λ k → tr< k t₁) lem23 x₁₀) (subst (λ k → tr< k t₂) lem23 x₂) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) ti₁ lem22)  where
+       lem23 : key₁ ≡ 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 _ _ _ )) refl ti))
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) () (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) 
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) () (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) () (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄  rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄  rbt) = ⊥-elim (⊥-color ceq)   
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) () rbr-leaf
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) x₁
+          (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) ti₁ lem22)  where
+       lem23 : key₁ ≡ 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 _ _ _ )) refl ti))
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-right {k₃} {_} {_} {t₃} {t₄} {t₅} x₆ x₇ rbt) = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04)
+          (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) (proj1 (proj2 rr04)) rr02 ti₁ lem22)  where
+       lem23 : key₁ ≡ 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 _ _ _ )) refl ti))
+       rr02 : tr> k t₃
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04)) 
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-left {k₃} {_} {_} {t₃} {t₄} {t₅} x₆ x₇ rbt) = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04)
+          (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) rr02 (proj2 (proj2 rr04)) ti₁ lem22)  where
+       lem23 : key₁ ≡ 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 _ _ _ )) refl ti))
+       rr02 : tr> k t₃
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04)) 
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-right {t₃} {t₄} {t₅} x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-left {t₃} {t₄} {t₅} x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-ll  {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ rbt) 
+    = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04)
+          (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) 
+             ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ ( tr>-to-black (proj2 (proj2 rr04))) ti₁ lem22)  where
+       lem23 : key₁ ≡ 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 _ _ _ )) refl ti))
+       rr02 : tr> k t₂
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr04))) )
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-lr {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ x₉ rbt) 
+    = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04)
+          (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) 
+             ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , rr02 ⟫ ⟫ ( tr>-to-black (proj2 (proj2 rr04))) ti₁ lem22)  where
+       lem23 : key₁ ≡ 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 _ _ _ )) refl ti))
+       rr02 : tr> k t₂
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr04))) )
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rl {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ x₉ rbt) 
+    = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04)
+          (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) 
+             (tr>-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫  ti₁ lem22)  where
+       lem23 : key₁ ≡ 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 _ _ _ )) refl ti))
+       rr02 : tr> k t₂
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr04))) )
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rr {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ rbt) 
+    = subst treeInvariant
+     (node-cong refl refl (just-injective (cong node-left eq)) refl) (t-node _ _ _ (subst (λ j → key₃ < j) lem23 x) (proj1 rr04)
+          (subst (λ k → tr< k t₇) lem23 x₂) (subst (λ k → tr< k t₈) lem23 x₃) 
+             (tr>-to-black (proj1 (proj2 rr04)))  ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj1 (proj2 (proj2 (proj2 rr04))) , rr02 ⟫ ⟫  ti₁ lem22)  where
+       lem23 : key₁ ≡ 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 _ _ _ )) refl ti))
+       rr02 : tr> k t₂
+       rr02 = RB-repl→ti> _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr04))) )
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rr x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-ll x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
+
+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 {n} {A} {key} {value} {t} {t1} {t2} {v1} {k} ceq x₁ rbt prev ti = lem21 (node k ⟪ Black , v1 ⟫ t1 t) ti refl rbt where 
+  lem22 : treeInvariant t2
+  lem22 = prev (treeLeftDown _ _ ti )
+  lem21 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node k ⟪ Black , v1 ⟫ t1 t → replacedRBTree key value t1 t2  → treeInvariant (node k ⟪ Black , v1 ⟫ t2 t)
+  lem21 _ t-leaf () rbt
+  lem21 _ (t-single key value) eq rbr-leaf = subst treeInvariant (node-cong refl refl refl (just-injective (cong node-right eq)) ) (t-left _ _ x₁ _ _ lem22) 
+  lem21 _ (t-single key value) () (rbr-node {_} {_} {t₃} {t₄})
+  lem21 _ (t-single key value) () (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt)
+  lem21 _ (t-single key value) () (rbr-left  {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) 
+  lem21 _ (t-single key value) () (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) 
+  lem21 _ (t-single key value) () (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) 
+  lem21 _ (t-single key value) () (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) 
+  lem21 _ (t-single key value) () (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) 
+  lem21 _ (t-single key value) () (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) 
+  lem21 _ (t-single key value) () (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) 
+  lem21 _ (t-single key value) () (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) 
+  lem21 _ (t-single key value) () (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) 
+  lem21 _ (t-single key value) () (rbr-rotate-rl  {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) 
+  lem21 _ (t-single key value) () (rbr-rotate-lr {t} {t₁} {uncle}  t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) 
+  lem21 _ (t-right key₂ key₁ {v1} {v2} {t} {t₁} x x₁₀ x₂ ti₁) eq rbr-leaf = subst treeInvariant (node-cong refl refl refl (just-injective (cong node-right eq)) ) 
+    (t-node _ _ _ x₁ (subst (λ j →  j < key₁) lem23 x) tt tt (subst (λ k → tr> k t) lem23 x₁₀ ) (subst (λ k → tr> k t₁) lem23 x₂ ) (t-single _ _) ti₁) where
+       lem23 : key₂ ≡ k
+       lem23 = just-injective (cong node-key eq)
+  lem21 _ (t-right key₂ key₁ {v1} {v2} {t} {t₁} x x₁₀ x₂ ti₁) () (rbr-node {_} {_} {t₃} {t₄}) 
+  lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) 
+  lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) 
+  lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) 
+  lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂}x₃ x₄ rbt) 
+  lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) 
+  lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) 
+  lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) 
+  lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) () (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) 
+  lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄  rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄  rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-right key₂ key₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t} {t₁} x x₁₀ x₂ ti₁) () rbr-leaf 
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) lem22 )  where
+       rr04 : (key < k) ∧ tr< k t₃ ∧ tr< k t₄ 
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-right {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) rr02 lem22 )  where
+       rr04 : (k₁ < k) ∧ tr< k t₄ ∧ tr< k t₅ 
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr< k t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04)) 
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-left {k₁} {_} {_} {t₃} {t₄} {t₅} x₃ x₄ rbt) = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) rr02 (proj2 (proj2 rr04)) lem22 )  where
+       rr04 : (k₁ < k) ∧ tr< k t₄ ∧ tr< k t₅ 
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr< k t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04)) 
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) ⟪ proj1 (proj1 (proj2 rr04)) , 
+         ⟪ rr02 , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr04))) lem22 )  where
+       rr04 : (kg < k) ∧ ((kp < k) ∧ tr< k t₂ ∧ tr< k t₁) ∧ tr< k uncle
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr< k t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr04))) ) 
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-lr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) ⟪ proj1 (proj1 (proj2 rr04)) , 
+         ⟪ proj1 (proj2 (proj1 (proj2 rr04))) ,  rr02 ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr04))) lem22 )  where
+       rr04 : (kg < k) ∧ ((kp < k) ∧ tr< k t₁ ∧ tr< k t₂) ∧ tr< k uncle
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr< k t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr04))) ) 
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-rl {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) (tr<-to-black (proj1 (proj2 rr04)))
+         ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ lem22 )  where
+       rr04 : (kg < k) ∧ tr< k uncle ∧ ((kp < k) ∧ tr< k t₂ ∧ tr< k t₁)
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr< k t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr04))) ) 
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-left _ _ (proj1 rr04) (tr<-to-black (proj1 (proj2 rr04))) 
+         ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj1 (proj2 (proj2 (proj2 rr04))) , rr02 ⟫ ⟫ lem22 )  where
+       rr04 : (kg < k) ∧ tr< k uncle ∧ ((kp < k) ∧ tr< k t₁ ∧ tr< k t₂)
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr< k t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr04))) ) 
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄  rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄  rbt) = ⊥-elim (⊥-color ceq)   
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) () rbr-leaf
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-node {_} {_} {t₃} {t₄}) = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
+          (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) (subst (λ j → tr> j t₁₀) lem23 x₄) (subst (λ j → tr> j t₁₁) lem23 x₅)  lem22 ti₂) where
+       lem23 : key₁ ≡ k
+       lem23 = just-injective (cong node-key eq) 
+       rr04 : (key < k) ∧ tr< k t₃ ∧ tr< k t₄ 
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-right {k₃} {_} {_} {t₃} {t₄} {t₅} x₆ x₇ rbt) = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
+          (proj1 (proj2 rr04)) rr02 (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅)  lem22 ti₂)  where
+       lem23 : key₁ ≡ k
+       lem23 = just-injective (cong node-key eq) 
+       rr04 : (k₃ < k) ∧ tr< k t₄ ∧ tr< k t₅
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr< k t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr04)) 
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-left {k₃} {_} {_} {t₃} {t₄} {t₅} x₆ x₇ rbt) = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
+          rr02 (proj2 (proj2 rr04)) (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅) lem22 ti₂)  where
+       lem23 : key₁ ≡ k
+       lem23 = just-injective (cong node-key eq) 
+       rr04 : (k₃ < k) ∧ tr< k t₄ ∧ tr< k t₅ 
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr< k t₃
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr04)) 
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-right {t₃} {t₄} {t₅} x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-left {t₃} {t₄} {t₅} x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-ll  {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ rbt) 
+    = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
+          ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫  (tr<-to-black (proj2 (proj2 rr04))) (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅)  lem22 ti₂)  where
+       lem23 : key₁ ≡ k
+       lem23 = just-injective (cong node-key eq) 
+       rr04 : (kg < k) ∧ ((kp < k) ∧ tr< k t₁ ∧ tr< k t) ∧ tr< k uncle
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr< k t₂
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr04))) )
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-lr {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ x₉ rbt) 
+    = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
+          ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , rr02 ⟫ ⟫  (tr<-to-black (proj2 (proj2 rr04))) (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅)  lem22 ti₂)  where
+       lem23 : key₁ ≡ k
+       lem23 = just-injective (cong node-key eq) 
+       rr04 : (kg < k) ∧ ((kp < k) ∧ tr< k t ∧ tr< k t₁) ∧ tr< k uncle 
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr< k t₂
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj1 (proj2 rr04))) )
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rl {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ x₉ rbt) 
+    = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
+          (tr<-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ rr02 , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫  (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅)  lem22 ti₂)  where
+       lem23 : key₁ ≡ k
+       lem23 = just-injective (cong node-key eq) 
+       rr04 : (kg < k) ∧ tr< k uncle ∧ ((kp < k) ∧ tr< k t₁ ∧ tr< k t)
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr< k t₂
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr04))) )
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₉} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rr {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x₆ x₇ x₈ rbt) 
+    = subst treeInvariant
+     (node-cong refl refl refl (just-injective (cong node-right eq))) (t-node _ _ _ (proj1 rr04) (subst (λ j → j < key₂) lem23 x₁₀)
+          (tr<-to-black (proj1 (proj2 rr04))) ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj1 (proj2 (proj2 (proj2 rr04))) , rr02 ⟫ ⟫  (subst (λ k → tr> k t₉) lem23 x₄) (subst (λ k → tr> k t₁₀) lem23 x₅)  lem22 ti₂)  where
+       lem23 : key₁ ≡ k
+       lem23 = just-injective (cong node-key eq) 
+       rr04 : (kg < k) ∧ tr< k uncle ∧ ((kp < k) ∧ tr< k t ∧ tr< k t₁)
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr02 : tr< k t₂
+       rr02 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr04))) )
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rr x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-ll x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
+
+
+
+to-black-treeInvariant : {n : Level} {A : Set n} → (t : bt (Color ∧ A) ) → treeInvariant t → treeInvariant (to-black t)
+to-black-treeInvariant {n} {A} .leaf t-leaf = t-leaf
+to-black-treeInvariant {n} {A} .(node key value leaf leaf) (t-single key value) = t-single key _
+to-black-treeInvariant {n} {A} .(node key _ leaf (node key₁ _ _ _)) (t-right key key₁ x x₁ x₂ ti) = t-right key key₁ x x₁ x₂ ti 
+to-black-treeInvariant {n} {A} .(node key₁ _ (node key _ _ _) leaf) (t-left key key₁ x x₁ x₂ ti) = t-left key key₁ x x₁ x₂ ti 
+to-black-treeInvariant {n} {A} .(node key₁ _ (node key _ _ _) (node key₂ _ _ _)) (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) = t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁
+
+RB→t2notLeaf : {n : Level} {A : Set n} {key : ℕ} {value : A} → (t₁ t₂ : bt (Color ∧ A) ) → (rbt : replacedRBTree key value t₁ t₂) → IsNode t₂ 
+RB→t2notLeaf {n} {A} {k} {v} .leaf .(node k ⟪ Red , v ⟫ leaf leaf) rbr-leaf = record { key = k ; value = ⟪ Red , v ⟫ ; left = leaf ; right = leaf ; t=node = refl } 
+RB→t2notLeaf {n} {A} {k} {v} .(node k ⟪ _ , _ ⟫ _ _) .(node k ⟪ _ , v ⟫ _ _) rbr-node = record { key = k ; value = ⟪ _ , v ⟫ ; left = _ ; right = _ ; t=node = refl }
+RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-right x x₁ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
+RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-left x x₁ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
+RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-right x x₁ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
+RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-left x x₁ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
+RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-ll x x₁ x₂ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
+RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-lr x x₁ x₂ x₃ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
+RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rl x x₁ x₂ x₃ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
+RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rr x x₁ x₂ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
+RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) (rbr-rotate-ll x x₁ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
+RB→t2notLeaf {n} {A} {k} {v} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) (rbr-rotate-rr x x₁ rbt) = record { key = _ ; value = _ ; left = _ ; right = _; t=node = refl }
+RB→t2notLeaf {n} {A} {k} {v} .(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₂ rbt) = record { key = kn ; value = ⟪ Black , _ ⟫ ; left = _ ; right = _; t=node = refl }
+RB→t2notLeaf {n} {A} {k} {v} .(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₂ rbt) = record { key = kn ; value = ⟪ Black , _ ⟫ ; left = _ ; right = _; t=node = refl }
+
+
+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 {n} {A} {key} {value} {t} {t1} {t2} {uncle} {kg} {kp} {vg} {vp} ceq ueq x₁ rbt prev ti 
+     = lem21 (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t1 t) uncle) ti refl rbt where 
+  lem22 : treeInvariant t2
+  lem22 = prev (treeLeftDown _ _ (treeLeftDown _ _ ti ))
+  lem25 : treeInvariant t
+  lem25 = treeRightDown _ _ (treeLeftDown _ _ ti)
+  lem21 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t1 t) uncle) → replacedRBTree key value t1 t2  
+      → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t2 t) (to-black uncle))
+  lem21 _ t-leaf () rbt
+  lem21 _ (t-single key value) () _
+  lem21 _ (t-right key key₁ x x₁₀ x₂ ti₁) () _
+  lem21 _ (t-left key₂ key₁ {_} {_} {t} {t₁} x x₁₀ x₂ ti₁) eq rbr-leaf = subst treeInvariant (node-cong refl refl refl (subst (λ k → leaf ≡ to-black k ) lem24 refl) )
+     (t-left _ _ (proj1 rr04) ⟪ rr07 , ⟪ tt , tt ⟫ ⟫  (proj2 (proj2 rr04))  (subst (λ k → treeInvariant (node kp ⟪ Black , vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) k )) 
+          (just-injective (cong node-right (just-injective (cong node-left eq)))) (rr05 t₁ refl rr06) )) where
+       lem24 : leaf ≡ uncle
+       lem24 = just-injective (cong node-right eq) 
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       rr04 : (kp < kg) ∧ ⊤ ∧ tr< kg _
+       rr04 = proj1 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) refl ti))
+       rr06 : treeInvariant t₁
+       rr06 = treeRightDown _ _ ti₁
+       rr07 : key < kg
+       rr07 = <-trans x₁ (proj1 rr04)
+       rr05 : (tree : bt (Color ∧ A)) → tree ≡ t₁ → treeInvariant tree → treeInvariant (node kp ⟪ Black , vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) tree)
+       rr05 .leaf eq₁ t-leaf = t-left _ _ x₁ tt tt (t-single _ _)
+       rr05 .(node key₃ value leaf leaf) eq₁ ti₃@(t-single key₃ value) = t-node _ _ _ x₁ rr09 tt tt tt tt (t-single _ _) (t-single _ _) where
+           rr08 : (key₂ < key₃) ∧ ⊤ ∧ ⊤
+           rr08 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (node-cong refl refl refl (sym eq₁)) ti₁))
+           rr09 : kp < key₃
+           rr09 = subst (λ k →  k < key₃) (just-injective (cong node-key (just-injective (cong node-left eq)))) (proj1 rr08)
+       rr05 .(node key₃ _ leaf (node key₁ _ _ _)) eq₁ ti₃@(t-right key₃ key₁ {_} {_} {t₃} {t₄} x x₁₀ x₂ ti₂) = t-node _ _ _ x₁ (proj1 rr08) tt tt tt 
+              ⟪ <-trans (proj1 rr08) x , ⟪ proj1 (proj2 (proj2 (proj2 rr08))) , proj2 (proj2 (proj2 (proj2 rr08))) ⟫ ⟫ (t-single _ _) ti₃ where
+           rr08 : (kp < key₃) ∧ ⊤ ∧ ((kp < key₁) ∧ tr> kp t₃ ∧ tr> kp t₄)
+           rr08 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (node-cong (just-injective (cong node-key (just-injective (cong node-left eq)))) refl refl (sym eq₁)) ti₁))
+       rr05 .(node key₁ _ (node key₃ _ _ _) leaf) eq₁ ti₃@(t-left key₃ key₁ {_} {_} {t₃} {t₄} x x₁₀ x₂ ti₂) = t-node _ _ _ x₁ (proj1 rr08) tt tt 
+              (proj1 (proj2 rr08)) tt (t-single _ _) ti₃ where
+           rr08 : (kp < key₁) ∧ ((kp < key₃) ∧ tr> kp t₃ ∧ tr> kp t₄) ∧ ⊤
+           rr08 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (node-cong (just-injective (cong node-key (just-injective (cong node-left eq)))) refl refl (sym eq₁)) ti₁))
+       rr05 .(node key₁ _ (node key₃ _ _ _) (node key₂ _ _ _)) eq₁ ti₄@(t-node key₃ key₁ key₂ {_} {_} {_} {t₃} {t₄} {t₅} {t₆} x x₁₀ x₂ x₃ x₄ x₅ ti₂ ti₃) 
+         = t-node _ _ _ x₁ (proj1 rr08) tt tt (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) (t-single _ _) ti₄ where
+           rr08 : (kp < key₁) ∧ ((kp < key₃) ∧ tr> kp t₃ ∧ tr> kp t₄) ∧ ((kp < key₂) ∧ tr> kp t₅ ∧ tr> kp t₆)
+           rr08 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (node-cong (just-injective (cong node-key (just-injective (cong node-left eq)))) refl refl (sym eq₁)) ti₁))
+  lem21 _ (t-left key₂ key₁ {value₁} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-node {v₁} {ca} {t₃} {t₄}) = rr05 t refl lem25 where 
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       lem24 : leaf ≡ uncle
+       lem24 = just-injective (cong node-right eq) 
+       rr04 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ tr< kg t
+       rr04 = proj1 (ti-property1 ti)
+       rr08 : (key < kp) ∧ tr< kp t₃ ∧ tr< kp t₄
+       rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
+       rr05 : (tree : bt (Color ∧ A)) → tree ≡ t → treeInvariant tree  
+            → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ (node key ⟪ ca , value ⟫ t₃ t₄) t) (to-black uncle))
+       rr05 _ eq₁ t-leaf = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)  (subst (λ k → leaf ≡ to-black k ) lem24 refl))
+         ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) tt (t-left _ _ x₁ (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) lem22  )) 
+       rr05 _ eq₁ (t-single key₃ value) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)  
+         (subst (λ k → leaf ≡ to-black k ) lem24 refl)) 
+         ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ tt , tt ⟫ ⟫ 
+             (t-node _ _ _ (proj1 rr08) rr10 (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) tt tt lem22  (t-single _ _) ))  where
+           rr09 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ ((key₃ < kg) ∧ ⊤ ∧ ⊤ )
+           rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ ca , v₁ ⟫ t₃ t₄) k) uncle)) 
+               (sym eq₁) ti))
+           rr10 : kp < key₃ 
+           rr10 = proj1 (subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti))))
+       rr05 _ eq₁ (t-right key₃ key₁ {_} {_} {t₅} {t₆} y y₁ y₂ ti₁) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)  
+         (subst (λ k → leaf ≡ to-black k ) lem24 refl)) 
+         ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ tt , proj2 (proj2 (proj2 (proj2 rr09))) ⟫ ⟫ 
+             (t-node _ _ _ (proj1 rr08) rr10 (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) tt 
+             ⟪ <-trans rr10 y , ⟪ <-tr> y₁ rr10 , <-tr> y₂ rr10 ⟫ ⟫ lem22  (t-right _ _ y y₁ y₂ ti₁) ))  where
+           rr09 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ ((key₃ < kg) ∧ ⊤ ∧ ( (key₁ < kg) ∧ tr< kg t₅ ∧ tr< kg t₆ ) )
+           rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ ca , v₁ ⟫ t₃ t₄) k) uncle)) 
+               (sym eq₁) ti))
+           rr10 : kp < key₃ 
+           rr10 = proj1 (subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti))))
+       rr05 _ eq₁ (t-left key₃ key₁ {_} {_} {t₅} {t₆} y y₁ y₂ ti₁) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)  
+         (subst (λ k → leaf ≡ to-black k ) lem24 refl)) 
+         ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ proj1 (proj2 (proj2 (proj2 rr09))) , tt ⟫ ⟫ 
+             (t-node _ _ _ (proj1 rr08) (proj1 rr10) (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) 
+             ⟪ proj1 (proj1 (proj2 rr10)) , ⟪ proj1 (proj2 (proj1 (proj2 rr10))) , proj2 (proj2 (proj1 (proj2 rr10))) ⟫ ⟫ tt lem22  (t-left _ _ y y₁ y₂ ti₁) ))  where
+           rr09 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ ((key₁ < kg) ∧ ( (key₃ < kg) ∧ tr< kg t₅ ∧ tr< kg t₆ ) ∧ ⊤ ) 
+           rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ ca , v₁ ⟫ t₃ t₄) k) uncle)) 
+               (sym eq₁) ti))
+           rr10 : (kp < key₁ ) ∧ ((kp < key₃) ∧ tr> kp t₅ ∧ tr> kp t₆) ∧ ⊤ 
+           rr10 = subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+       rr05 _ eq₁ (t-node key₃ key₁ key₂ {_} {_} {_} {t₅} {t₆} {t₇} {t₈} y y₁ y₂ y₃ y₄ y₅ ti₁ ti₂) 
+        = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)  
+         (subst (λ k → leaf ≡ to-black k ) lem24 refl)) 
+         ( t-left _ _ (proj1 rr04) (proj1 (proj2 rr04)) ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ proj1 (proj2 (proj2 (proj2 rr09))) , proj2 (proj2 (proj2 (proj2 rr09))) ⟫ ⟫
+             (t-node _ _ _ (proj1 rr08) (proj1 rr10) (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) 
+             ⟪ proj1 (proj1 (proj2 rr10)) , ⟪ proj1 (proj2 (proj1 (proj2 rr10))) , proj2 (proj2 (proj1 (proj2 rr10))) ⟫ ⟫ (proj2 (proj2 rr10)) lem22  
+                (t-node _ _ _ y y₁ y₂ y₃ y₄ y₅ ti₁ ti₂)))  where
+           rr09 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ ((key₁ < kg) ∧ ( (key₃ < kg) ∧ tr< kg t₅ ∧ tr< kg t₆ ) ∧ ( (key₂ < kg) ∧ tr< kg t₇ ∧ tr< kg t₈ ) )
+           rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ ca , v₁ ⟫ t₃ t₄) k) uncle)) 
+               (sym eq₁) ti))
+           rr10 : (kp < key₁ ) ∧ ((kp < key₃) ∧ tr> kp t₅ ∧ tr> kp t₆) ∧ ((kp < key₂) ∧ tr> kp t₇ ∧ tr> kp t₈)
+           rr10 = subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-right {k₁} {v₁} {ca} {t₃} {t₄} {t₅} x₃ x₄ rbt) = rr05 t refl lem25 where 
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       lem24 : leaf ≡ uncle
+       lem24 = just-injective (cong node-right eq) 
+       rr04 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ tr< kg t
+       rr04 = proj1 (ti-property1 ti)
+       rr08 : (k₁ < kp) ∧ tr< kp t₄ ∧ tr< kp t₅
+       rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
+       rr03 : tr< kp t₃
+       rr03 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr08))
+       rr05 : (tree : bt (Color ∧ A)) → tree ≡ t → treeInvariant tree  
+          → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₃) t) (to-black uncle))
+       rr05 _ eq₁ t-leaf = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)  (subst (λ k → leaf ≡ to-black k ) lem24 refl))
+         ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫  tt 
+             (t-left _ _ (proj1 rr08) (proj1 (proj2 rr08)) rr03 lem22  ))  
+       rr05 _ eq₁ (t-single key₃ value) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)  
+         (subst (λ k → leaf ≡ to-black k ) lem24 refl)) 
+         ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04)   , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫  ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ tt , tt ⟫ ⟫ 
+             (t-node _ _ _ (proj1 rr08) rr10 (proj1 (proj2 rr08)) rr03 tt tt lem22  (t-single _ _) ))  where
+           rr09 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ ((key₃ < kg) ∧ ⊤ ∧ ⊤ )
+           rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₅) k) uncle)) 
+               (sym eq₁) ti))
+           rr10 : kp < key₃ 
+           rr10 = proj1 (subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti))))
+       rr05 _ eq₁ (t-right key₃ key₁ {_} {_} {t₆} {t₇} y y₁ y₂ ti₁) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)  
+         (subst (λ k → leaf ≡ to-black k ) lem24 refl)) 
+         ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ proj1 (proj2 (proj1 (proj2 rr04)))  , >-tr< rr03 (proj1 rr04) ⟫ ⟫ ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ tt , proj2 (proj2 (proj2 (proj2 rr09))) ⟫ ⟫ 
+             (t-node _ _ _ (proj1 rr08) rr10 (proj1 (proj2 rr08)) rr03 tt 
+             ⟪ <-trans rr10 y , ⟪ <-tr> y₁ rr10 , <-tr> y₂ rr10 ⟫ ⟫ lem22  (t-right _ _ y y₁ y₂ ti₁) ))  where
+           rr09 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ ((key₃ < kg) ∧ ⊤ ∧ ( (key₁ < kg) ∧ tr< kg t₆ ∧ tr< kg t₇ ) )
+           rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₅) k) uncle)) 
+               (sym eq₁) ti))
+           rr10 : kp < key₃ 
+           rr10 = proj1 (subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti))))
+       rr05 _ eq₁ (t-left key₃ key₁ {_} {_} {t₆} {t₇} y y₁ y₂ ti₁) = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)  
+         (subst (λ k → leaf ≡ to-black k ) lem24 refl)) 
+         ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫ ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ proj1 (proj2 (proj2 (proj2 rr09))) , tt ⟫ ⟫ 
+             (t-node _ _ _ (proj1 rr08) (proj1 rr10) (proj1 (proj2 rr08)) rr03 
+             ⟪ proj1 (proj1 (proj2 rr10)) , ⟪ proj1 (proj2 (proj1 (proj2 rr10))) , proj2 (proj2 (proj1 (proj2 rr10))) ⟫ ⟫ tt lem22  (t-left _ _ y y₁ y₂ ti₁) ))  where
+           rr09 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ ((key₁ < kg) ∧ ( (key₃ < kg) ∧ tr< kg t₆ ∧ tr< kg t₇ ) ∧ ⊤ ) 
+           rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₅) k) uncle)) 
+               (sym eq₁) ti))
+           rr10 : (kp < key₁ ) ∧ ((kp < key₃) ∧ tr> kp t₆ ∧ tr> kp t₇) ∧ ⊤ 
+           rr10 = subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+       rr05 _ eq₁ (t-node key₃ key₁ key₂ {_} {_} {_} {t₆} {t₇} {t₈} {t₉} y y₁ y₂ y₃ y₄ y₅ ti₁ ti₂) 
+        = subst treeInvariant (node-cong refl refl (node-cong refl refl refl eq₁)  
+         (subst (λ k → leaf ≡ to-black k ) lem24 refl)) 
+         ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04)  , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫ ⟪ proj1 (proj2 (proj2 rr09)) , ⟪ proj1 (proj2 (proj2 (proj2 rr09))) , proj2 (proj2 (proj2 (proj2 rr09))) ⟫ ⟫
+             (t-node _ _ _ (proj1 rr08) (proj1 rr10) (proj1 (proj2 rr08)) rr03 
+             ⟪ proj1 (proj1 (proj2 rr10)) , ⟪ proj1 (proj2 (proj1 (proj2 rr10))) , proj2 (proj2 (proj1 (proj2 rr10))) ⟫ ⟫ (proj2 (proj2 rr10)) lem22  
+                (t-node _ _ _ y y₁ y₂ y₃ y₄ y₅ ti₁ ti₂)))  where
+           rr09 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ ((key₁ < kg) ∧ ( (key₃ < kg) ∧ tr< kg t₆ ∧ tr< kg t₇ ) ∧ ( (key₂ < kg) ∧ tr< kg t₈ ∧ tr< kg t₉ ) )
+           rr09 = proj1 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₄ t₅) k) uncle)) 
+               (sym eq₁) ti))
+           rr10 : (kp < key₁ ) ∧ ((kp < key₃) ∧ tr> kp t₆ ∧ tr> kp t₇) ∧ ((kp < key₂) ∧ tr> kp t₈ ∧ tr> kp t₉)
+           rr10 = subst (λ k → tr> kp k) (sym eq₁) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti₁) eq (rbr-left {k₁} {v₁} {ca} {t₃} {t₄} {t₅} x₃ x₄ rbt) = 
+       subst treeInvariant (node-cong refl refl refl (subst (λ k → leaf ≡ to-black k ) lem24 refl))
+         ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪  >-tr< rr03 (proj1 rr04) , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (proj2 (proj2 rr04)) rr06) where
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       lem24 : leaf ≡ uncle
+       lem24 = just-injective (cong node-right eq) 
+       rr04 : (kp < kg) ∧ ((k₁ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ tr< kg t
+       rr04 = proj1 (ti-property1 ti)
+       rr08 : (k₁ < kp) ∧ tr< kp t₄ ∧ tr< kp t₅
+       rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
+       rr03 : tr< kp t₃
+       rr03 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr08))
+       rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node k₁ ⟪ ca , v₁ ⟫ t₃ t₅) t)
+       rr06 with node→leaf∨IsNode t
+       ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) rr03 (proj2 (proj2 rr08)) lem22  )
+       ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) rr03 (proj2 (proj2 rr08)) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) 
+                lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
+           rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)   
+           rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = 
+       subst treeInvariant (node-cong refl refl refl (subst (λ k → leaf ≡ to-black k ) lem24 refl))
+         ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪  proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr03 (proj1 rr04) ⟫ ⟫ (proj2 (proj2 rr04)) rr06) where
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       lem24 : leaf ≡ uncle
+       lem24 = just-injective (cong node-right eq) 
+       rr04 : (kp < kg) ∧ ((_ < kg) ∧ tr< kg t₁ ∧ tr< kg t₂) ∧ tr< kg t
+       rr04 = proj1 (ti-property1 ti)
+       rr08 : (_ < kp) ∧ tr< kp t₁ ∧ tr< kp t₂
+       rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
+       rr03 : tr< kp t₃
+       rr03 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr08))
+       rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node _ ⟪ _ , _ ⟫ t₁ t₃) t)
+       rr06 with node→leaf∨IsNode t
+       ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (proj1 (proj2 rr08)) rr03 lem22  )
+       ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) (proj1 (proj2 rr08)) 
+          rr03 (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
+           rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)   
+           rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = 
+       subst treeInvariant (node-cong refl refl refl (subst (λ k → leaf ≡ to-black k ) lem24 refl))
+         ( t-left _ _ (proj1 rr04) ⟪ <-trans (proj1 rr08) (proj1 rr04) , ⟪  >-tr< rr03 (proj1 rr04) , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (proj2 (proj2 rr04)) rr06 ) where
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       lem24 : leaf ≡ uncle
+       lem24 = just-injective (cong node-right eq) 
+       rr04 : (kp < kg) ∧ ((_ < kg) ∧ tr< kg t₂ ∧ tr< kg t₁) ∧ tr< kg t
+       rr04 = proj1 (ti-property1 ti)
+       rr08 : (_ < kp) ∧ tr< kp t₂ ∧ tr< kp t₁
+       rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
+       rr03 : tr< kp t₃
+       rr03 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr08))
+       rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node _ ⟪ _ , _ ⟫ t₃ t₁) t)
+       rr06 with node→leaf∨IsNode t
+       ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) rr03 (proj2 (proj2 rr08)) lem22  )
+       ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) rr03
+          (proj2 (proj2 rr08)) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
+           rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)   
+           rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-ll {t₁} {t₂} {t₃} {t₆} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) 
+     = ⊥-elim (⊥-color (trans (sym lem26) ueq) ) where
+       lem26 : color uncle ≡ Black
+       lem26 = subst (λ k → color k ≡ Black) (just-injective (cong node-right eq )) refl
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-lr {t₁} {t₂} {t₃} {t₆} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) 
+     = ⊥-elim (⊥-color (trans (sym lem26) ueq) ) where
+       lem26 : color uncle ≡ Black
+       lem26 = subst (λ k → color k ≡ Black) (just-injective (cong node-right eq )) refl
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-rl {t₁} {t₂} {t₃} {t₆} {kg} {kp} {vg} {vp} x₃ x₄ x₅ x₆ rbt) 
+     = ⊥-elim (⊥-color (trans (sym lem26) ueq) ) where
+       lem26 : color uncle ≡ Black
+       lem26 = subst (λ k → color k ≡ Black) (just-injective (cong node-right eq )) refl
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-flip-rr {t₁} {t₂} {t₃} {t₆} {kg} {kp} {vg} {vp} x₃ x₄ x₅ rbt) 
+     = ⊥-elim (⊥-color (trans (sym lem26) ueq) ) where
+       lem26 : color uncle ≡ Black
+       lem26 = subst (λ k → color k ≡ Black) (just-injective (cong node-right eq )) refl
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄  rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄  rbt) = ⊥-elim (⊥-color ceq)   
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-left key₂ key₁ {_} {_} {t₄} {t₅} x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq  rbr-leaf = 
+    subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (proj1 rr03) ⟪ <-trans x₁ (proj1 rr04) , ⟪ tt , tt ⟫ ⟫  (proj2 (proj2 rr04)) 
+      (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) rr06 (to-black-treeInvariant _ ti₂)) where
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       lem24 :  node key₂ v2 t₁₀ t₁₁ ≡ uncle
+       lem24 = just-injective (cong node-right eq)
+       rr04 : (kp < kg) ∧ ⊤ ∧ tr< kg t
+       rr04 = proj1 (ti-property1 ti)
+       rr03 : (kg < key₂) ∧ tr> kg t₁₀ ∧ tr> kg t₁₁
+       rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ _ t) k)) (sym lem24) ti))
+       rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ _ t)
+       rr06 with node→leaf∨IsNode t
+       ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ x₁ tt tt lem22  )
+       ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ x₁ (proj1 rr11) tt 
+          tt (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
+           rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)   
+           rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-node {_} {_} {t₃} {t₄}) = 
+    subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (proj1 rr03) (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) 
+      (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) rr06 (to-black-treeInvariant _ ti₂)) where
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       lem24 :  node key₂ v2 t₁₀ t₁₁ ≡ uncle
+       lem24 = just-injective (cong node-right eq)
+       rr04 : (kp < kg) ∧ ((key < kg) ∧ tr< kg t₃ ∧ tr< kg t₄) ∧ tr< kg t
+       rr04 = proj1 (ti-property1 ti)
+       rr08 : (key < kp) ∧ tr< kp t₃ ∧ tr< kp t₄
+       rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
+       rr03 : (kg < key₂) ∧ tr> kg t₁₀ ∧ tr> kg t₁₁
+       rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node key ⟪ _ , _ ⟫ t₃ t₄) t) k)) (sym lem24) ti))
+       rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node _ ⟪ _ , _ ⟫ t₃ t₄) t)
+       rr06 with node→leaf∨IsNode t
+       ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (proj1 (proj2 rr08)) (proj2 (proj2 rr08)) lem22  )
+       ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) (proj1 (proj2 rr08)) 
+          (proj2 (proj2 rr08)) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
+           rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)   
+           rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-right {k₃} {_} {_} {t₃} {t₄} {t₅} x₆ x₇ rbt) = 
+    subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (proj1 rr03) 
+     ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , >-tr< rr05 (proj1 rr04) ⟫ ⟫ (proj2 (proj2 rr04)) 
+      (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) rr06 (to-black-treeInvariant _ ti₂)) where
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       lem24 :  node key₂ v2 t₁₀ t₁₁ ≡ uncle
+       lem24 = just-injective (cong node-right eq)
+       rr04 : (kp < kg) ∧ ((k₃ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ tr< kg t
+       rr04 = proj1 (ti-property1 ti)
+       rr08 : (k₃ < kp) ∧ tr< kp t₄ ∧ tr< kp t₅
+       rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
+       rr03 : (kg < key₂) ∧ tr> kg t₁₀ ∧ tr> kg t₁₁
+       rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₃ ⟪ _ , _ ⟫ t₄ t₅) t) k)) (sym lem24) ti))
+       rr05 : tr< kp t₃
+       rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 rr08))
+       rr06 : treeInvariant (node kp ⟪ Black , vp ⟫ (node k₃ ⟪ _ , _ ⟫ t₄ t₃) t)
+       rr06 with node→leaf∨IsNode t
+       ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (proj1 (proj2 rr08)) rr05 lem22)
+       ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) (proj1 (proj2 rr08)) 
+          rr05 (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
+           rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)   
+           rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-left {k₃} {_} {_} {t₃} {t₄} {t₅} x₆ x₇ rbt) = 
+    subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (proj1 rr03) 
+     ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ >-tr< rr05 (proj1 rr04)  , proj2 (proj2 (proj1 (proj2 rr04))) ⟫ ⟫ (proj2 (proj2 rr04)) 
+      (proj1 (proj2 rr03)) (proj2 (proj2 rr03)) rr06 (to-black-treeInvariant _ ti₂)) where
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       lem24 :  node key₂ v2 t₁₀ t₁₁ ≡ uncle
+       lem24 = just-injective (cong node-right eq)
+       rr04 : (kp < kg) ∧ ((k₃ < kg) ∧ tr< kg t₄ ∧ tr< kg t₅) ∧ tr< kg t
+       rr04 = proj1 (ti-property1 ti)
+       rr08 : (k₃ < kp) ∧ tr< kp t₄ ∧ tr< kp t₅
+       rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
+       rr03 : (kg < key₂) ∧ tr> kg t₁₀ ∧ tr> kg t₁₁
+       rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ (node k₃ ⟪ _ , _ ⟫ t₄ t₅) t) k)) (sym lem24) ti))
+       rr05 : tr< kp t₃
+       rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 rr08))
+       rr06 :  treeInvariant (node kp ⟪ Black , vp ⟫ (node k₃ ⟪ _ , _ ⟫ t₃ t₅) t)
+       rr06 with node→leaf∨IsNode t
+       ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) rr05 (proj2 (proj2 rr08)) lem22)
+       ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) rr05 
+          (proj2 (proj2 rr08)) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
+           rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)   
+           rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-right {t₃} {t₄} {t₅} x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-left {t₃} {t₄} {t₅} x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-ll  {t₄} {t₁} {t₂} {t₃} {kg₁} {kp₁} {vg₁} {vp₁} x₆ x₇ x₈ rbt) =
+    subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (subst (λ k → k < key₂) lem23 (proj1 rr03)) 
+     ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ ⟪ <-trans (proj1 (proj1 (proj2 rr08))) (proj1 rr04)  , 
+        ⟪ >-tr< rr05 (proj1 rr04) , proj2 (proj2 (proj1 (proj2 (proj1 (proj2 rr04))))) ⟫ ⟫ , tr<-to-black (proj2 (proj2 (proj1 (proj2 rr04)))) ⟫ ⟫ (proj2 (proj2 rr04)) 
+      (subst (λ k → tr> k t₁₀) lem23 (proj1 (proj2 rr03))) (subst (λ k → tr> k t₁₁) lem23 (proj2 (proj2 rr03))) rr06 (to-black-treeInvariant _ ti₂)) where
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       lem24 :  node key₂ v2 t₁₀ t₁₁ ≡ uncle
+       lem24 = just-injective (cong node-right eq)
+       rr04 : (kp < kg) ∧ ((kg₁ < kg) ∧ ((kp₁ < kg) ∧ tr< kg t₁ ∧ tr< kg t₄) ∧ tr< kg t₃ )  ∧ tr< kg t
+       rr04 = proj1 (ti-property1 ti)
+       rr08 : (kg₁ < kp) ∧ ((kp₁ < kp) ∧ tr< kp t₁ ∧ tr< kp t₄) ∧ tr< kp t₃ 
+       rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
+       rr03 : (key₁ < key₂) ∧ tr> key₁ t₁₀ ∧ tr> key₁ t₁₁ 
+       rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (sym eq) ti ))
+       rr05 : tr< kp t₂
+       rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj1 (proj2 rr08))))
+       rr06 :  treeInvariant (node kp ⟪ Black , vp ⟫ (node kg₁ ⟪ Red , vg₁ ⟫ (node kp₁ ⟪ Black , vp₁ ⟫ t₂ t₄) (to-black t₃)) t)
+       rr06 with node→leaf∨IsNode t
+       ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) ⟪ proj1 (proj1 (proj2 rr08)) , 
+           ⟪ rr05 , proj2 (proj2 (proj1 (proj2 rr08))) ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr08))) lem22)
+       ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) 
+           ⟪ proj1 (proj1 (proj2 rr08)) , ⟪ rr05 , proj2 (proj2 (proj1 (proj2 rr08))) ⟫ ⟫ 
+          (tr<-to-black (proj2 (proj2 rr08))) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
+           rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)   
+           rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-lr {t₀} {t₁} {t₂} {t₃} {kg₁} {kp₁} {vg₁} {vp₁} x₆ x₇ x₈ x₉ rbt) =
+    subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (subst (λ k → k < key₂) lem23 (proj1 rr03)) 
+     ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ ⟪ <-trans (proj1 (proj1 (proj2 rr08))) (proj1 rr04)  , 
+        ⟪ proj1 (proj2 (proj1 (proj2 (proj1 (proj2 rr04))))) , >-tr< rr05 (proj1 rr04) ⟫ ⟫ , tr<-to-black (proj2 (proj2 (proj1 (proj2 rr04)))) ⟫ ⟫ (proj2 (proj2 rr04)) 
+      (subst (λ k → tr> k t₁₀) lem23 (proj1 (proj2 rr03))) (subst (λ k → tr> k t₁₁) lem23 (proj2 (proj2 rr03))) rr06 (to-black-treeInvariant _ ti₂)) where
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       lem24 :  node key₂ v2 t₁₀ t₁₁ ≡ uncle
+       lem24 = just-injective (cong node-right eq)
+       rr04 : (kp < kg) ∧ ((kg₁ < kg) ∧ ((kp₁ < kg) ∧ tr< kg t₀ ∧ tr< kg t₁) ∧ tr< kg t₃ )  ∧ tr< kg t
+       rr04 = proj1 (ti-property1 ti)
+       rr08 : (kg₁ < kp) ∧ ((kp₁ < kp) ∧ tr< kp t₀ ∧ tr< kp t₁) ∧ tr< kp t₃ 
+       rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
+       rr03 : (key₁ < key₂) ∧ tr> key₁ t₁₀ ∧ tr> key₁ t₁₁ 
+       rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (sym eq) ti ))
+       rr05 : tr< kp t₂
+       rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁  (proj2 (proj2 (proj1 (proj2 rr08))))
+       rr06 :  treeInvariant (node kp ⟪ Black , vp ⟫ (node kg₁ ⟪ Red , vg₁ ⟫ (node kp₁ ⟪ Black , _ ⟫ t₀ t₂) (to-black t₃)) t)
+       rr06 with node→leaf∨IsNode t
+       ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) ⟪ proj1 (proj1 (proj2 rr08)) , 
+           ⟪ proj1 (proj2 (proj1 (proj2 rr08))) , rr05 ⟫ ⟫ (tr<-to-black (proj2 (proj2 rr08))) lem22)
+       ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) 
+           ⟪ proj1 (proj1 (proj2 rr08)) , ⟪ proj1 (proj2 (proj1 (proj2 rr08))) , rr05 ⟫ ⟫ 
+          (tr<-to-black (proj2 (proj2 rr08))) (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
+           rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)   
+           rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rl {t₀} {t₁} {t₂} {t₃} {kg₁} {kp₁} {vg₁} {vp₁} x₆ x₇ x₈ x₉ rbt)  = 
+    subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (subst (λ k → k < key₂) lem23 (proj1 rr03)) 
+     ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ 
+          tr<-to-black (proj1 (proj2 (proj1 (proj2 rr04))))   , ⟪ proj1 (proj2 (proj2 (proj1 (proj2 rr04)))) , 
+            ⟪ >-tr< rr05 (proj1 rr04) , proj2 (proj2 (proj2 (proj2 (proj1 (proj2 rr04))))) ⟫ ⟫ ⟫ ⟫ (proj2 (proj2 rr04)) 
+      (subst (λ k → tr> k t₁₀) lem23 (proj1 (proj2 rr03))) (subst (λ k → tr> k t₁₁) lem23 (proj2 (proj2 rr03))) rr06 (to-black-treeInvariant _ ti₂)) where
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       lem24 :  node key₂ v2 t₁₀ t₁₁ ≡ uncle
+       lem24 = just-injective (cong node-right eq)
+       rr04 : (kp < kg) ∧ ((kg₁ < kg) ∧ tr< kg t₃ ∧ ((kp₁ < kg) ∧ tr< kg t₁ ∧ tr< kg t₀) ) ∧ tr< kg t
+       rr04 = proj1 (ti-property1 ti)
+       rr08 : (kg₁ < kp) ∧ tr< kp t₃ ∧ ((kp₁ < kp) ∧ tr< kp t₁ ∧ tr< kp t₀) 
+       rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
+       rr03 : (key₁ < key₂) ∧ tr> key₁ t₁₀ ∧ tr> key₁ t₁₁ 
+       rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (sym eq) ti ))
+       rr05 : tr< kp t₂
+       rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj1 (proj2 (proj2 (proj2 rr08))))
+       rr06 :   treeInvariant (node kp ⟪ Black , vp ⟫ (node kg₁ ⟪ Red , vg₁ ⟫ (to-black t₃) (node kp₁ ⟪ Black , vp₁ ⟫ t₂ t₀)) t)
+       rr06 with node→leaf∨IsNode t
+       ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (tr<-to-black (proj1 (proj2 rr08))) 
+         ⟪ proj1 (proj2 (proj2 rr08)) , ⟪ rr05 , proj2 (proj2 (proj2 (proj2 rr08))) ⟫ ⟫  lem22)
+       ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) 
+          (tr<-to-black (proj1 (proj2 rr08))) ⟪ proj1 (proj2 (proj2 rr08)) , ⟪ rr05 , proj2 (proj2 (proj2 (proj2 rr08))) ⟫ ⟫  
+              (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
+           rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)   
+           rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} {t₁₁} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-flip-rr {t₀} {t₁} {t₂} {t₃} {kg₁} {kp₁} {vg₁} {vp₁} x₆ x₇ x₈ rbt) =
+    subst treeInvariant (node-cong refl refl refl (cong to-black lem24) ) ( t-node _ _ _ (proj1 rr04) (subst (λ k → k < key₂) lem23 (proj1 rr03)) 
+     ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ 
+          tr<-to-black (proj1 (proj2 (proj1 (proj2 rr04))))   , ⟪ proj1 (proj2 (proj2 (proj1 (proj2 rr04)))) , 
+            ⟪ proj1 (proj2 (proj2 (proj2 (proj1 (proj2 rr04))))) , >-tr< rr05 (proj1 rr04) ⟫ ⟫ ⟫ ⟫ (proj2 (proj2 rr04)) 
+      (subst (λ k → tr> k t₁₀) lem23 (proj1 (proj2 rr03))) (subst (λ k → tr> k t₁₁) lem23 (proj2 (proj2 rr03))) rr06 (to-black-treeInvariant _ ti₂)) where
+       lem23 : key₁ ≡ kg
+       lem23 = just-injective (cong node-key eq) 
+       lem24 :  node key₂ v2 t₁₀ t₁₁ ≡ uncle
+       lem24 = just-injective (cong node-right eq)
+       rr04 : (kp < kg) ∧ ((kg₁ < kg) ∧ tr< kg t₃ ∧ ((kp₁ < kg) ∧ tr< kg t₀ ∧ tr< kg t₁) ) ∧ tr< kg t
+       rr04 = proj1 (ti-property1 ti)
+       rr08 : (kg₁ < kp) ∧ tr< kp t₃ ∧ ((kp₁ < kp) ∧ tr< kp t₀ ∧ tr< kp t₁) 
+       rr08 = proj1 (ti-property1 (treeLeftDown _ _ ti))
+       rr03 : (key₁ < key₂) ∧ tr> key₁ t₁₀ ∧ tr> key₁ t₁₁ 
+       rr03 = proj2 (ti-property1 (subst (λ k → treeInvariant k) (sym eq) ti ))
+       rr05 : tr< kp t₂
+       rr05 = RB-repl→ti< _ _ _ _ _ rbt x₁ (proj2 (proj2 (proj2 (proj2 rr08))))
+       rr06 :  treeInvariant (node kp ⟪ Black , vp ⟫ (node kg₁ ⟪ Red , vg₁ ⟫ (to-black t₃) (node kp₁ ⟪ Black , vp₁ ⟫ t₀ t₂)) t)
+       rr06 with node→leaf∨IsNode t
+       ... | case1 eq₁ = subst treeInvariant (node-cong refl refl refl (sym eq₁)) (t-left _ _ (proj1 rr08) (tr<-to-black (proj1 (proj2 rr08))) 
+         ⟪ proj1 (proj2 (proj2 rr08)) , ⟪ proj1 (proj2 (proj2 (proj2 rr08))) , rr05 ⟫ ⟫  lem22)
+       ... | case2 tn = subst treeInvariant (node-cong refl refl refl (sym (IsNode.t=node tn))) ( t-node _ _ _ (proj1 rr08) (proj1 rr11) 
+          (tr<-to-black (proj1 (proj2 rr08))) ⟪ proj1 (proj2 (proj2 rr08)) , ⟪ proj1 (proj2 (proj2 (proj2 rr08))) , rr05 ⟫ ⟫  
+              (proj1 (proj2 rr11)) (proj2 (proj2 rr11)) lem22 (subst treeInvariant (IsNode.t=node tn) lem25 )) where
+           rr11 : (kp < IsNode.key tn) ∧ tr> kp (IsNode.left tn) ∧ tr> kp (IsNode.right tn)   
+           rr11 = subst (λ k → tr> kp k) (IsNode.t=node tn) (proj2 (ti-property1 (treeLeftDown _ _ ti)))
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rr x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-ll x₆ x₇ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
+  lem21 _ (t-node key₃ key₁ key₂ {v0} {v1} {v2} {t₇} {t₈} {t₁₀} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) = ⊥-elim (⊥-color ceq)
+
+
+
+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 {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)))) 
+