--- a/redBlackTreeTest.agda	Thu Jan 11 15:16:44 2018 +0900
+++ b/redBlackTreeTest.agda	Thu Jan 11 17:38:13 2018 +0900
@@ -38,11 +38,19 @@
     \t x -> check1 x 1 ≡ True   )))
 test2 = refl
 
-test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 
-    $ \t -> putTree1 t 2 2 
-    $ \t -> getRedBlackTree t 2 
-    $ \t x -> check1 x 2 ≡ True  
-test3 = {!!} -- refl
+test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 
+    $ \t -> putTree1 t 2 2
+    $ \t -> putTree1 t 3 3
+    $ \t -> putTree1 t 4 4
+    $ \t -> getRedBlackTree t 4
+    $ \t x -> check1 x 4 ≡ True  
+test3 = refl
+
+test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 
+    $ \t -> putTree1 t 2 2
+    $ \t -> putTree1 t 3 3
+    $ \t -> putTree1 t 4 4
+    $ \t -> root t
 
 -- test4 : putTree1 {_} {_} {ℕ} {ℕ} ( createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $  \t -> putTree1 t 2 2  $ \t ->
 --   root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )