-- {-# 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))))