diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index b2d3d9b..7284786 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1888,13 +1888,33 @@ Proof.
 
   assert (V: 3 < n). generalize I. generalize H.
   apply tm_step_palindromic_length_12_n.
+  destruct n. inversion V. destruct n. inversion V. inversion H1.
+
+  rewrite K in H. rewrite L in H. rewrite M in H.
+  rewrite tm_morphism_twice_rev in H.
+  rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
+  rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
+  rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
+  rewrite <- tm_step_lemma in H. rewrite <- tm_step_lemma in H.
+  rewrite <- tm_morphism_eq in H. rewrite <- tm_morphism_eq in H.
+  rewrite Nat.pred_succ in H. rewrite Nat.pred_succ in H.
+
+  pose (hd' := (firstn (length hd / 4) (tm_step n))).
+  pose (a' := (firstn (length a / 4) (skipn (length hd / 4) (tm_step n)))).
+  pose (tl' := (skipn (length hd / 4 + Nat.div2 (length a)) (tm_step n))).
+  fold hd' in H. fold a' in H. fold tl' in H.
+
+  rewrite Nat.pred_succ in L. rewrite Nat.pred_succ in L.
+  assert (N: length a = length a). reflexivity.
+  rewrite L in N at 2. fold a' in N.
+  rewrite tm_morphism_length in N. rewrite tm_morphism_length in N.
+  rewrite Nat.mul_assoc in N. replace (2*2) with 4 in N.
 
   induction m.
-  - rewrite K in H. rewrite L in H. rewrite M in H.
-    rewrite tm_morphism_twice_rev in H.
-    rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
-    rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
-    rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
+  - assert (even (length (hd' ++ a')) = true).
+
+
+