diff --git a/src/thue_morse2.v b/src/thue_morse2.v
index abfab56..cd2d374 100644
--- a/src/thue_morse2.v
+++ b/src/thue_morse2.v
@@ -17,27 +17,74 @@ Proof.
   assert (I: even (length hd) = false).
   assert (J: {even (length hd) = false} + { ~ (even (length hd)) = false}).
   apply bool_dec. destruct J. assumption. apply not_false_is_true in n0.
+  assert (K: count_occ Bool.bool_dec hd true
+           = count_occ Bool.bool_dec hd false).
+  generalize n0. generalize H. apply tm_step_count_occ.
   rewrite app_assoc in H.
-  assert (K: count_occ Bool.bool_dec (hd ++ [b1;b1]) true
+  assert (L: count_occ Bool.bool_dec (hd ++ [b1;b1]) true
            = count_occ Bool.bool_dec (hd ++ [b1;b1]) false).
   assert (even (length (hd ++ [b1;b1])) = true).
   rewrite app_length. rewrite Nat.even_add_even. assumption.
   simpl. apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
   generalize H0. generalize H. apply tm_step_count_occ.
+  rewrite count_occ_app in L. rewrite count_occ_app in L.
+  rewrite K in L. rewrite Nat.add_cancel_l in L.
+  destruct b1. simpl in L. inversion L. simpl in L. inversion L.
+
+  assert (J: {even (length (hd ++ [b1;b1] ++ a))
+            = false} + { ~ (even (length (hd ++ [b1;b1] ++ a))) = false}).
+  apply bool_dec. destruct J.
+
+  rewrite app_length in e. rewrite app_length in e.
+  rewrite Nat.add_assoc in e. rewrite Nat.add_shuffle0 in e.
+  rewrite Nat.even_add_even in e. rewrite Nat.even_add in e.
+  rewrite I in e. destruct (Nat.even (length a)). reflexivity.
+  simpl in e. inversion e. simpl.
+  apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
+
+  apply not_false_is_true in n0.
+  assert (K: even (length (hd ++ [b1;b1] ++ a ++ [b2;b2])) = true).
+  replace (hd ++ [b1;b1] ++ a ++ [b2;b2])
+    with ((hd ++ [b1;b1] ++ a) ++ [b2;b2]).
+  rewrite app_length. rewrite Nat.even_add.
+  rewrite n0. reflexivity.
+  rewrite <- app_assoc. apply app_inv_head_iff.
+  rewrite <- app_assoc. reflexivity.
+
+  assert (N: count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a ++ [b2;b2]) true
+    = count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a ++ [b2;b2]) false).
+  replace (hd ++ [b1;b1] ++ a ++ [b2;b2] ++ tl)
+    with ((hd ++ [b1;b1] ++ a ++ [b2;b2]) ++ tl) in H.
+  generalize K. generalize H. apply tm_step_count_occ.
+  rewrite <- app_assoc. apply app_inv_head_iff.
+  rewrite <- app_assoc. apply app_inv_head_iff.
+  rewrite <- app_assoc. reflexivity.
+
+  assert (M: count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a) true
+    = count_occ Bool.bool_dec (hd ++ [b1;b1] ++ a) false).
+  replace (hd ++ [b1;b1] ++ a ++ [b2;b2] ++ tl)
+    with ((hd ++ [b1;b1] ++ a) ++ [b2;b2] ++ tl) in H.
+  generalize n0. generalize H. apply tm_step_count_occ.
+  rewrite <- app_assoc. apply app_inv_head_iff.
+  rewrite <- app_assoc. reflexivity.
+
+  replace (hd ++ [b1;b1] ++ a ++ [b2;b2])
+    with ((hd ++ [b1;b1] ++ a) ++ [b2;b2]) in N.
+  rewrite count_occ_app in N. symmetry in N.
+  rewrite count_occ_app in N. rewrite M in N.
+  rewrite Nat.add_cancel_l in N.
+  destruct b2. simpl in N. inversion N. simpl in N. inversion N.
+  rewrite <- app_assoc. apply app_inv_head_iff.
+  rewrite <- app_assoc. reflexivity.
+Qed.
 
 
 
-  destruct n.
-  - simpl in H. destruct hd. simpl in H. assert (b1 = false).
-    inversion H. rewrite H0 in H. inversion H. inversion H.
-    symmetry in H2. apply app_eq_nil in H2. destruct H2. inversion H2.
-  - rewrite <- tm_step_lemma in H.
-    assert (I: even (length hd) = false).
-    assert (J: {even (length hd) = false} + { ~ (even (length hd)) = false}).
-    apply bool_dec. destruct J. assumption. apply not_false_is_true in n0.
 
 
 
+  
+
 Theorem tm_step_count_occ : forall (hd tl : list bool) (n : nat),
   tm_step n = hd ++ tl -> even (length hd) = true
   -> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false.