# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1523415461 -32400
# Node ID ba7c5f1c293797ad36c10a2633f5f56747647843
# Parent  40ab3d39e49d54695585e7ca162b60dc3b445419
this slightly better

diff -r 40ab3d39e49d -r ba7c5f1c2937 redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Wed Apr 11 11:29:57 2018 +0900
+++ b/redBlackTreeTest.agda	Wed Apr 11 11:57:41 2018 +0900
@@ -11,7 +11,6 @@
 
 
 open import Algebra
-open import Relation.Binary
 open import Data.Nat.Properties   as NatProp
 
 open Tree
@@ -247,10 +246,10 @@
       lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y
       lemma2 = refl
 
-open IsStrictTotalOrder
 
 compTri :  ( x y : ℕ ) ->  Tri  (x < y) ( x ≡ y )  ( x > y )
 compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) 
+   where open import  Relation.Binary
 
 checkT : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool {m}
 checkT Nothing _ = False
@@ -258,6 +257,16 @@
 ...  | tri≈ _ _ _ = True
 ...  | _ = False
 
+checkEQ :  {m : Level }  ( x :  ℕ ) -> ( n : Node  ℕ ℕ ) -> (value n )  ≡ x  -> checkT {m} (Just n) x ≡ True
+checkEQ x n refl with compTri (value n)  x
+... |  tri≈ _ _ _ = refl
+... |  _ = {!!}
+
+checkT' : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool {m}
+checkT' Nothing _ = False
+checkT' (Just n) x with (value n) ≟ x
+...  | yes _ = True
+...  | no _  = False
 
 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ))
          → (k : ℕ) (x : ℕ)