redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} -> RedBlackTree {Level.zero} {m} {t} a ℕ
redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }

putTest1Lemma2 : (k : ℕ)  -> compare2 k k ≡ EQ
putTest1Lemma2 zero = refl
putTest1Lemma2 (suc k) = putTest1Lemma2 k

putTest1Lemma1 : (x y : ℕ)  -> compareℕ x y ≡ compare2 x y
putTest1Lemma1 zero    zero    = refl
putTest1Lemma1 (suc m) zero    = refl
putTest1Lemma1 zero    (suc n) = refl
putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n
putTest1Lemma1 (suc .m)           (suc .(Data.Nat.suc m + k)) | less    m k = lemma1  m
 where
    lemma1 : (m :  ℕ) -> LT  ≡ compare2 m (ℕ.suc (m + k))
    lemma1  zero = refl
    lemma1  (suc y) = lemma1 y
putTest1Lemma1 (suc .m)           (suc .m)           | equal   m   = lemma1 m
 where
    lemma1 : (m :  ℕ) -> EQ  ≡ compare2 m m
    lemma1  zero = refl
    lemma1  (suc y) = lemma1 y
putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m)           | greater m k = lemma1 m
 where
    lemma1 : (m :  ℕ) -> GT  ≡ compare2  (ℕ.suc (m + k))  m
    lemma1  zero = refl
    lemma1  (suc y) = lemma1 y

putTest1Lemma3 : (k : ℕ)  -> compareℕ k k ≡ EQ
putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k  )

compareLemma1 : {x  y : ℕ}  -> compare2 x y ≡ EQ -> x  ≡ y
compareLemma1 {zero} {zero} refl = refl
compareLemma1 {zero} {suc _} ()
compareLemma1 {suc _} {zero} ()
compareLemma1 {suc x} {suc y} eq = cong ( \z -> ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) )
   where
     lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
      lemma2 = refl

putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
         -> (k : ℕ) (x : ℕ)
         -> putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
         (\ t -> getRedBlackTree t k (\ t x1 -> check2 x1 x  ≡ True))
putTest1 n k x with n
...  | Just n1 = lemma2 ( record { top = Nothing } )
   where
     lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) -> putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
         GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
     lemma2 s with compare2 k (key n1)
     ... |  EQ = lemma3 {!!}
        where
           lemma3 : compare2 k (key n1) ≡  EQ -> getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
               key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
               } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y  } ) k ( \ t x1 -> check2 x1 x  ≡ True)
           lemma3 eq with compare2 x x | putTest1Lemma2 x
           ... | EQ | refl with compare2 k (key n1)  | eq
           ...              | EQ | refl with compare2 x x | putTest1Lemma2 x
           ...                    | EQ | refl = refl
     ... |  GT = {!!}
     ... |  LT = {!!}

...  | Nothing =  lemma1
   where
     lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red
        } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y  } ) k
        ( \ t x1 -> check2 x1 x  ≡ True)
     lemma1 with compare2 k k | putTest1Lemma2 k
     ... | EQ | refl with compare2 x x | putTest1Lemma2 x
     ...              | EQ | refl = refl