diff --git a/src/coalgebras/ltreeScript.sml b/src/coalgebras/ltreeScript.sml
index e046770bdb..97705cdff4 100644
--- a/src/coalgebras/ltreeScript.sml
+++ b/src/coalgebras/ltreeScript.sml
@@ -1187,15 +1187,22 @@ Proof
  >> rw [LNTH_IS_SOME, LFINITE_LLENGTH]
 QED
 
+Theorem ltree_el_ltree_delete :
+    !f p t. ltree_el t p = SOME (a,SOME (SUC n)) ==>
+          ltree_el (ltree_delete f t p) p = SOME (a,SOME n)
+Proof
+    cheat
+QED
+
 (* NOTE: “ltree_el t p = SOME (a,SOME (SUC n)” indicates that “SNOC n p” is the
    subtree to be deleted.
  *)
-Theorem ltree_paths_ltree_delete :
+Theorem ltree_delete_paths :
     !f p t a n.
        ltree_el t p = SOME (a,SOME (SUC n)) ==>
        ltree_paths (ltree_delete f t p) =
        ltree_paths t DIFF
-         (IMAGE (\q. p ++ [n] ++ q)
+         (IMAGE (\q. SNOC n p ++ q)
                 (ltree_paths (THE (ltree_lookup t (SNOC n p)))))
 Proof
     Q.X_GEN_TAC ‘f’
@@ -1236,7 +1243,113 @@ Proof
        Cases_on ‘LNTH n ts’ >> fs [] ])
  (* stage work *)
  >> rpt STRIP_TAC
- >> cheat
+ >> ‘!q. SNOC n (h::p) ++ q = h::(SNOC n p ++ q)’ by rw []
+ >> POP_ORW
+ >> ‘SNOC n (h::p) = h::SNOC n p’ by rw []
+ >> POP_ORW
+ >> Cases_on ‘t’
+ >> POP_ASSUM MP_TAC
+ >> simp [ltree_el_def, ltree_lookup_def]
+ >> Cases_on ‘LNTH h ts’ >> simp []
+ >> DISCH_TAC
+ >> MP_TAC (Q.SPECL [‘f’, ‘a'’, ‘ts’, ‘h’, ‘p’, ‘x’] ltree_delete_CONS)
+ >> simp []
+ >> DISCH_THEN K_TAC
+ >> simp [Once ltree_paths_alt_ltree_el]
+ >> simp [Once EXTENSION]
+ >> Q.X_GEN_TAC ‘ns’
+ >> EQ_TAC >> rw []
+ >| [ (* goal 1 (of 3) *)
+      Cases_on ‘ns’ >> fs [ltree_el_def, LNTH_LGENLIST] \\
+      POP_ASSUM MP_TAC \\
+      Cases_on ‘LLENGTH ts’ >> simp []
+      >- (Cases_on ‘h' = h’ >> simp []
+          >- (POP_ASSUM K_TAC \\
+              DISCH_TAC \\
+              Know ‘t IN ltree_paths (ltree_delete f x p)’
+              >- rw [ltree_paths_alt_ltree_el] \\
+              Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
+              simp [] >> DISCH_THEN K_TAC \\
+              rw [ltree_paths_alt_ltree_el, ltree_el_def]) \\
+          rw [ltree_paths_alt_ltree_el, ltree_el_def] \\
+          Cases_on ‘LNTH h' ts’ >> simp []
+          >- (Know ‘~LFINITE ts’ >- rw [LFINITE_LLENGTH] \\
+              DISCH_TAC \\
+              fs [infinite_lnth_some] \\
+              POP_ASSUM (MP_TAC o Q.SPEC ‘h'’) >> rw []) \\
+          fs []) \\
+      rename1 ‘LLENGTH ts = SOME N’ \\
+      Cases_on ‘h' < N’ >> simp [] \\
+      Cases_on ‘h' = h’ >> simp []
+      >- (POP_ASSUM (fs o wrap) \\
+          DISCH_TAC \\
+          Know ‘t IN ltree_paths (ltree_delete f x p)’
+          >- rw [ltree_paths_alt_ltree_el] \\
+          Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
+          simp [] >> DISCH_THEN K_TAC \\
+          rw [ltree_paths_alt_ltree_el, ltree_el_def]) \\
+      rw [ltree_paths_alt_ltree_el, ltree_el_def] \\
+      Cases_on ‘LNTH h' ts’ >> simp []
+      >- (‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
+          Know ‘IS_SOME (LNTH h' ts)’ >- rw [LFINITE_LNTH_IS_SOME] \\
+          rw [IS_SOME_EXISTS]) \\
+      fs [],
+      (* goal 2 (of 3) *)
+      POP_ASSUM MP_TAC \\
+      simp [ltree_el_def, LNTH_LGENLIST] \\
+      Cases_on ‘LLENGTH ts’ >> simp []
+      >- (DISCH_TAC \\
+          Know ‘p ++ [n] ++ q IN ltree_paths (ltree_delete f x p)’
+          >- rw [ltree_paths_alt_ltree_el] \\
+          Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
+          simp []) \\
+      rename1 ‘LLENGTH ts = SOME N’ \\
+      Cases_on ‘h < N’ >> simp [] \\
+      DISCH_TAC \\
+      Know ‘p ++ [n] ++ q IN ltree_paths (ltree_delete f x p)’
+      >- rw [ltree_paths_alt_ltree_el] \\
+      Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
+      simp [],
+      (* goal 3 (of 3) *)
+      Cases_on ‘ns’ >> fs []
+      >- (simp [ltree_el_def, LNTH_LGENLIST]) \\
+      simp [ltree_el_def, LNTH_LGENLIST] \\
+      Cases_on ‘LLENGTH ts’ >> simp []
+      >- (Cases_on ‘h' = h’ >> simp []
+          >- (POP_ASSUM (fs o wrap) \\
+              Know ‘ltree_el (ltree_delete f x p) t <> NONE <=>
+                    t IN ltree_paths (ltree_delete f x p)’
+              >- rw [ltree_paths_alt_ltree_el] >> Rewr' \\
+              Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
+              simp [] >> DISCH_THEN K_TAC \\
+              Q.PAT_X_ASSUM ‘h::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
+              simp [ltree_paths_alt_ltree_el, ltree_el_def]) \\
+          fs [] \\
+          Q.PAT_X_ASSUM ‘h'::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
+          simp [ltree_paths_alt_ltree_el, ltree_el_def] \\
+          Cases_on ‘LNTH h' ts’ >> simp []) \\
+      rename1 ‘LLENGTH ts = SOME N’ \\
+      Cases_on ‘h' < N’ >> simp []
+      >- (Cases_on ‘h' = h’ >> simp []
+          >- (POP_ASSUM (fs o wrap) \\
+              Know ‘ltree_el (ltree_delete f x p) t <> NONE <=>
+                    t IN ltree_paths (ltree_delete f x p)’
+              >- rw [ltree_paths_alt_ltree_el] >> Rewr' \\
+              Q.PAT_X_ASSUM ‘!t a n. P’ (MP_TAC o Q.SPECL [‘x’, ‘a’, ‘n’]) \\
+              simp [] >> DISCH_THEN K_TAC \\
+              Q.PAT_X_ASSUM ‘h::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
+              rw [ltree_paths_alt_ltree_el, ltree_el_def]) \\
+          fs [] \\
+          Q.PAT_X_ASSUM ‘h'::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
+          simp [ltree_paths_alt_ltree_el, ltree_el_def] \\
+          Cases_on ‘LNTH h' ts’ >> simp []) \\
+     ‘N <= h'’ by rw [] \\
+      Q.PAT_X_ASSUM ‘h'::t IN ltree_paths (Branch a' ts)’ MP_TAC \\
+      simp [ltree_paths_alt_ltree_el, ltree_el_def] \\
+      Cases_on ‘LNTH h' ts’ >> simp [] \\
+     ‘LFINITE ts’ by rw [LFINITE_LLENGTH] \\
+      Know ‘IS_SOME (LNTH h' ts)’ >- rw [IS_SOME_EXISTS] \\
+      simp [LFINITE_LNTH_IS_SOME] ]
 QED
 
 (* NOTE: “ltree_insert f t p t0” inserts t0 as the right-most children of the
@@ -1296,6 +1409,15 @@ Proof
  >> rw [gen_ltree_unchanged_extra]
 QED
 
+Theorem ltree_finite_insert :
+    !t. ltree_finite t ==>
+        !p d len. ltree_el t p = SOME (d,len) /\
+                  ltree_finite t0 ==> ltree_finite (ltree_insert f t p t0)
+Proof
+    HO_MATCH_MP_TAC ltree_finite_ind
+ >> cheat
+QED
+
 (* NOTE: These are simple versions not modifying ltree node data. *)
 Overload ltree_delete' = “ltree_delete I”
 Overload ltree_insert' = “ltree_insert I”
@@ -1623,20 +1745,30 @@ Proof
  >> Cases_on ‘ltree_lookup t x’ >> FULL_SIMP_TAC std_ss []
  >> rename1 ‘ltree_lookup t x = SOME t1’
  >> rpt (Q.PAT_X_ASSUM ‘T’ K_TAC)
- (* applying ltree_paths_ltree_delete *)
- >> cheat
- (* applying ltree_insert_delete'
+ (* applying ltree_delete_paths *)
+ >> MP_TAC (Q.SPECL [‘I’, ‘p’, ‘t’, ‘a'’, ‘i’] ltree_delete_paths)
+ >> simp []
+ >> DISCH_TAC
+ >> Q.PAT_X_ASSUM ‘!t. ltree_paths t HAS_SIZE n ==> ltree_finite t’
+      (MP_TAC o Q.SPEC ‘t'’)
+ >> impl_tac
+ >- (simp [HAS_SIZE, CARD_DIFF] \\
+    ‘s INTER {x} = {x}’ by ASM_SET_TAC [] >> POP_ORW \\
+     simp [])
+ >> DISCH_TAC (* ltree_finite t' *)
+ (* applying ltree_insert_delete' *)
  >> Know ‘t = ltree_insert' t' p t0’
  >- (simp [Abbr ‘t'’, Once EQ_SYM_EQ] \\
      MATCH_MP_TAC ltree_insert_delete' \\
      Q.EXISTS_TAC ‘i’ >> simp [] \\
-     STRONG_CONJ_TAC >- (Cases_on ‘ltree_lookup t x’ >> fs []) \\
-     DISCH_TAC \\
-     Q.PAT_X_ASSUM ‘THE (ltree_lookup t x) = t0’ K_TAC \\
-     simp [ltree_branching_def]
+     simp [ltree_branching_def])
  >> Rewr'
- >> cheat
-  *)
+ (* final goal: ltree_finite t' ==> ltree_finite (ltree_insert' t' p t0) *)
+ >> ‘ltree_finite t0’ by simp [ltree_finite, Abbr ‘t0’]
+ >> irule ltree_finite_insert >> art []
+ >> qexistsl_tac [‘a'’, ‘SOME i’]
+ >> qunabbrev_tac ‘t'’
+ >> MATCH_MP_TAC ltree_el_ltree_delete >> art []
 QED
 
 Theorem finite_ltree_paths_imp_ltree_finite[local] :