diff --git a/src/thue_morse.v b/src/thue_morse.v
index 9b1ab67..d41510a 100644
--- a/src/thue_morse.v
+++ b/src/thue_morse.v
@@ -1344,15 +1344,13 @@ Proof.
   assert (J: {a=b} + {~ a=b}). apply list_eq_dec. apply bool_dec.
   destruct J.
   - rewrite <- e in H.
-    assert (exists (hd a tl : list bool),
+    assert (J: exists (hd a tl : list bool),
       tm_step n = hd ++ a ++ a ++ a ++ tl /\ 0 < length a).
     exists hd. exists a. exists tl. split; assumption.
-    assert (exists (hd2 b tl2 : list bool),
-      tm_step 0 = hd2 ++ b ++ b ++ b ++ tl2 /\ 0 < length b).
-    generalize H0. apply tm_step_cube7.
-    destruct H1. destruct H1. destruct H1. destruct H1.
-    assert (0 < 0). generalize H2. generalize H1. apply tm_step_cube2.
-    apply Nat.lt_irrefl in H3. contradiction H3.
+    apply tm_step_cube7 in J.
+    destruct J. destruct H0. destruct H0. destruct H0.
+    assert (0 < 0). generalize H1. generalize H0. apply tm_step_cube2.
+    apply Nat.lt_irrefl in H2. contradiction H2.
   - assumption.
 Qed.