--- a/hoareBinaryTree.agda	Mon Nov 29 16:09:55 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 29 17:08:10 2021 +0900
@@ -297,9 +297,15 @@
 ... | tri< a ¬b ¬c | refl = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
     Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) 
     Post with replacePR.si Pre
-    ... | s-right x t = {!!}  -- can't happen
-    ... | s-left lt si with si-property1 si 
+    ... | s-left x t = {!!}  -- can't happen
+    ... | s-right lt si with si-property1 si 
     ... | refl = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = si  ; ri = repl04 ; ci = lift tt } where
+        repl05 : s-right lt si ≡ replacePR.si Pre → node key₁ value₁ left right ≡ child-replaced key value st tree1 (replacePR.tree0 Pre) si
+        repl05 = {!!}
+        repl06 : child-replaced key value (node key₁ value₁ left right ∷ st ) (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre) ≡ left
+        repl06 with replacePR.si Pre
+        ... | s-right x t = refl
+        ... | s-left x t = {!!}
         repl02 :  node key₁ value₁ (child-replaced key value
              (node key₁ value₁ left right ∷ st )
              (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre)) right