diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index d1ef1a1..9475711 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -2100,7 +2100,7 @@ Lemma tm_step_non_proper_palindrome_16 :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ (rev a) ++ tl
   -> length a = 8
-  -> skipn (length hd - 8) hd = rev (firstn 8 tl).
+  -> exists x, a = [x; negb x; negb x; x; negb x; x; x; negb x].
 Proof.
   intros n hd a tl. intros H I.
 
@@ -2223,6 +2223,16 @@ Proof.
   contradiction n1. reflexivity. reflexivity. reflexivity.
   rewrite H8 in H.
 
+  assert (b6 = negb b5). destruct b5; destruct b6.
+  contradiction H1. reflexivity. reflexivity. reflexivity.
+  contradiction H1. reflexivity. rewrite H9 in H.
+
+  exists b5. rewrite H4. rewrite H3. rewrite H8. rewrite H7. rewrite H5.
+  rewrite H0. rewrite H9. reflexivity.
+  reflexivity. inversion I. assumption. rewrite I.
+  rewrite <- Nat.le_succ_l. apply Nat.le_succ_diag_r.
+Qed.
+
 (*
 Lemma tm_step_proper_palindrome_center :
   forall (m n k : nat) (hd a tl : list bool),