diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index c28ebe2..0fa0fc8 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -2138,7 +2138,9 @@ Proof.
       ++ [b6; b5; b5; b3; b2; b1; b0; b] ++ tl)
     with ((hd ++ [b; b0; b1; b2; b3; b5; b5; b6; b6])
       ++ [b5] ++ [b5] ++ [b3] ++ [b2;b1;b0;b] ++ tl) in H.
-  apply tm_step_cubefree in H.
+  apply tm_step_cubefree in H. destruct b5; destruct b3.
+  contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
+  apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.