redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a !$\mathbb{N}$!)) {t : Set m} !$\rightarrow$! RedBlackTree {Level.zero} {m} {t} a !$\mathbb{N}$!
redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }

putTest1 :{ m : Level } (n : Maybe (Node !$\mathbb{N}$! !$\mathbb{N}$!))
         !$\rightarrow$! (k : !$\mathbb{N}$!) (x : !$\mathbb{N}$!)
         !$\rightarrow$! putTree1 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} (redBlackInSomeState {_} !$\mathbb{N}$! n {Set Level.zero}) k x
         (\ t !$\rightarrow$! getRedBlackTree t k (\ t x1 !$\rightarrow$! check2 x1 x  !$\equiv$! True))
putTest1 n k x with n
...  | Just n1 = lemma2 ( record { top = Nothing } )
   where
     lemma2 : (s : SingleLinkedStack (Node !$\mathbb{N}$! !$\mathbb{N}$!) ) !$\rightarrow$! putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (!$\lambda$! t !$\rightarrow$!
         GetRedBlackTree.checkNode t k (!$\lambda$! t!$\_{1}$! x1 !$\rightarrow$! check2 x1 x !$\equiv$! True) (root t))
     lemma2 s with compare2 k (key n1)
     ... |  EQ = lemma3 {!!}
        where
           lemma3 : compare2 k (key n1) !$\equiv$!  EQ !$\rightarrow$! getRedBlackTree {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} {Set Level.zero} ( record {  root = Just ( record {
               key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
               } ) ; nodeStack = s ; compare = !$\lambda$! x!$\_{1}$! y !$\rightarrow$! compare2 x!$\_{1}$! y  } ) k ( \ t x1 !$\rightarrow$! check2 x1 x  !$\equiv$! 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 {_} {_} {!$\mathbb{N}$!} {!$\mathbb{N}$!} {Set Level.zero} ( record {  root = Just ( record {
               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red
        } ) ; nodeStack = record { top = Nothing } ; compare = !$\lambda$! x!$\_{1}$! y !$\rightarrow$! compare2 x!$\_{1}$! y  } ) k
        ( \ t x1 !$\rightarrow$! check2 x1 x  !$\equiv$! True)
     lemma1 with compare2 k k | putTest1Lemma2 k
     ... | EQ | refl with compare2 x x | putTest1Lemma2 x
     ...              | EQ | refl = refl