--- a/redBlackTreeTest.agda	Wed Jan 17 18:28:25 2018 +0900
+++ b/redBlackTreeTest.agda	Thu Jan 18 10:38:55 2018 +0900
@@ -168,18 +168,20 @@
          -> 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
+...  | Just n1 = lemma2 ( record { top = Nothing } )
    where
-     lemma2 : putTree1 (record { root = Just n1 ; nodeStack = record { top = Nothing } ; compare = compare2 }) k x (λ t →
+     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 with compare2 k (key n1)
-     ... |  EQ = {!!}
+     lemma2 s with compare2 k (key n1)
+     ... |  EQ = lemma3 ?
         where 
-           lemma3 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
+           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 = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y  } ) k ( \ t x1 -> check2 x1 x  ≡ True)
-           lemma3 with compare2 x x | putTest1Lemma2 x 
-           ... | EQ | refl  = {!!}
+               } ) ; 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