diff --git a/src/thue_morse.v b/src/thue_morse.v
index 314ca28..63572f7 100644
--- a/src/thue_morse.v
+++ b/src/thue_morse.v
@@ -236,6 +236,14 @@ Proof.
     simpl. rewrite Nat.add_0_r. reflexivity.
 Qed.
 
+Lemma tm_morphism_length_half : forall (u : list bool),
+  Nat.div2 (length (tm_morphism u)) = length u.
+Proof.
+  intro u.
+  induction u. reflexivity.
+  simpl. rewrite IHu. reflexivity.
+Qed.
+
 Lemma tm_morphism_app : forall (l1 l2 : list bool),
   tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
 Proof.
diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index d6c1ca6..76d257d 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1575,38 +1575,46 @@ Proof.
   pose (tl' := skipn (Nat.div2 (length hd) + length a) (tm_step n)).
   fold hd' in H. fold a' in H. fold tl' in H.
 
-  assert (EVEN2: forall m, m mod 4 = 0 -> even (Nat.div2 m) = true).
-  intro m. intro U. rewrite <- Nat.div_exact in U.
-  rewrite U. replace 4 with (2*2). rewrite <- Nat.mul_assoc.
-  rewrite Nat.div2_double. rewrite Nat.even_mul. reflexivity. easy. easy.
-
-  assert (I': even (length hd') = true). unfold hd'. rewrite firstn_length.
-  assert (C: Nat.div2 (length hd) <= length (tm_step n)
-           \/ length (tm_step n) < Nat.div2 (length hd)).
-  apply Nat.le_gt_cases. destruct C.
-  apply Nat.min_r in H6. rewrite Nat.min_comm. rewrite H6.
-  apply EVEN2. assumption. apply Nat.lt_le_incl in H6.
-  apply Nat.min_l in H6. rewrite Nat.min_comm. rewrite H6.
-  rewrite tm_size_power2. destruct n. inversion V. inversion H8.
-  rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity.
-  apply Nat.le_0_l.
-
-  assert (J': even (length a') = true). unfold a'. rewrite firstn_length.
-  rewrite skipn_length.
-  assert (C: Nat.div2 (length a) <= length (tm_step n) - Nat.div2 (length hd)
-  \/ length (tm_step n) - Nat.div2 (length hd) < Nat.div2 (length a)).
-  apply Nat.le_gt_cases. destruct C.
-  apply Nat.min_r in H6. rewrite Nat.min_comm. rewrite H6. apply EVEN2.
-  assumption. apply Nat.lt_le_incl in H6.
-  apply Nat.min_l in H6. rewrite Nat.min_comm. rewrite H6.
-  rewrite tm_size_power2. destruct n. inversion V. inversion H8.
-  rewrite Nat.pow_succ_r. rewrite Nat.even_sub. rewrite Nat.even_mul.
-  assert (Nat.even (Nat.div2 (length hd)) = true). apply EVEN2. assumption.
-  rewrite H7. reflexivity.
+  assert (length hd' = Nat.div2 (length hd)). unfold hd'. rewrite H4.
+  rewrite tm_morphism_length_half. rewrite firstn_length. rewrite firstn_length.
+  replace (min (Nat.div2 (length hd)) (length (tm_step n)))
+    with (min (length (tm_step n)) (Nat.div2 (length hd))).
+  rewrite Nat.min_comm. rewrite Nat.min_assoc. rewrite Nat.min_id.
+  reflexivity. rewrite Nat.min_comm. reflexivity.
 
+  assert (length a' = Nat.div2 (length a)). unfold a'. rewrite H5.
+  rewrite tm_morphism_length_half. rewrite firstn_length. rewrite firstn_length.
+  rewrite Nat.min_comm. rewrite <- H6.
+  replace
+    (min (Nat.div2 (length a)) (length (skipn (length hd') (tm_step n))))
+    with 
+    (min (length (skipn (length hd') (tm_step n))) (Nat.div2 (length a))).
+  rewrite Nat.min_assoc. rewrite Nat.min_id. reflexivity.
+  rewrite Nat.min_comm. reflexivity.
 
+  assert (length tl' = Nat.div2 (length tl)). unfold tl'. rewrite H3.
+  rewrite tm_morphism_length_half. rewrite app_length.
+  symmetry. rewrite Nat.div2_div.
+  rewrite app_length. rewrite rev_length.
+  replace (length a + length a) with (length a * 2).
+  rewrite Nat.div_add. rewrite <- Nat.div2_div. reflexivity. easy.
+  rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
+
+  assert (I': even (length hd') = true). rewrite H6.
+  rewrite <- Nat.div_exact in J1. rewrite J1.
+  replace 4 with (2*2). rewrite <- Nat.mul_assoc. rewrite Nat.div2_double.
+  rewrite Nat.even_mul. reflexivity. reflexivity. easy.
+
+  assert (J': even (length a') = true). rewrite H7.
+  rewrite <- Nat.div_exact in J0. rewrite J0.
+  replace 4 with (2*2). rewrite <- Nat.mul_assoc. rewrite Nat.div2_double.
+  rewrite Nat.even_mul. reflexivity. reflexivity. easy.
+
+  assert (K': even (length (map negb (rev a'))) = true).
+  rewrite map_length. rewrite rev_length. assumption.
 
 
+Admitted.