--- a/redBlackTreeTest.agda	Wed Jan 17 17:31:41 2018 +0900
+++ b/redBlackTreeTest.agda	Wed Jan 17 18:28:25 2018 +0900
@@ -153,11 +153,11 @@
 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 x y ( trans lemma2 eq ) )
+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
@@ -168,7 +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 = {!!}
+...  | Just n1 = lemma2
+   where
+     lemma2 : putTree1 (record { root = Just n1 ; nodeStack = record { top = Nothing } ; compare = compare2 }) k x (λ t →
+         GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t))
+     lemma2 with compare2 k (key n1)
+     ... |  EQ = {!!}
+        where 
+           lemma3 : 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  = {!!}
+     ... |  GT = {!!}
+     ... |  LT = {!!}
 ...  | Nothing =  lemma1  
    where 
      lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {