--- a/BTree.agda	Fri Sep 13 13:25:17 2024 +0900
+++ b/BTree.agda	Sun Oct 06 17:59:51 2024 +0900
@@ -556,6 +556,25 @@
 
 open _∧_
 
+
+open _∧_
+
+record IsNode {n : Level} {A : Set n} (t : bt A) : Set (Level.suc n) where
+  field
+    key : ℕ
+    value : A
+    left : bt A
+    right : bt A
+    t=node : t ≡ node key value left right
+
+node→leaf∨IsNode : {n : Level} {A : Set n} → (t : bt A ) → (t ≡ leaf) ∨ IsNode t
+node→leaf∨IsNode leaf = case1 refl
+node→leaf∨IsNode (node key value t t₁) = case2 record { key = key ; value = value ; left = t ; right = t₁ ; t=node = refl }
+
+IsNode→¬leaf : {n : Level} {A : Set n} (t : bt A) → IsNode t →  ¬ (t ≡ leaf)
+IsNode→¬leaf .(node key value left right) record { key = key ; value = value ; left = left ; right = right ; t=node = refl } ()
+
+
 ri-tr>  : {n : Level} {A : Set n}  → (tree repl : bt A) → (key key₁ : ℕ) → (value : A)
      → replacedTree key value tree repl → key₁ < key → tr> key₁ tree → tr> key₁ repl
 ri-tr> .leaf .(node key value leaf leaf) key key₁ value r-leaf a tgt = ⟪ a , ⟪ tt , tt ⟫ ⟫