diff --git a/src/thue_morse.v b/src/thue_morse.v
index 860d13f..bebfc09 100644
--- a/src/thue_morse.v
+++ b/src/thue_morse.v
@@ -1138,45 +1138,43 @@ Proof.
     rewrite H5 in H9. rewrite Nat.add_cancel_l in H9.
 
     destruct b; destruct b0.
-    reflexivity.
-    rewrite count_occ_app in H9. rewrite count_occ_app in H9.
-    rewrite count_occ_cons_eq in H9. rewrite count_occ_cons_neq in H9.
-    rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
-    rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
-    rewrite count_occ_app in H5. rewrite count_occ_app in H5.
-    rewrite count_occ_cons_neq in H5. rewrite count_occ_cons_eq in H5.
-    rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
-    rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
-    rewrite H5 in H9.
-    rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
-    rewrite <- Nat.add_0_r in H9. rewrite <- Nat.add_assoc in H9.
-    rewrite Nat.add_cancel_l in H9. inversion H9.
-    reflexivity. easy. easy. reflexivity.
-    rewrite count_occ_app in H9. rewrite count_occ_app in H9.
-    rewrite count_occ_cons_neq in H9. rewrite count_occ_cons_eq in H9.
-    rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
-    rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
-    rewrite count_occ_app in H5. rewrite count_occ_app in H5.
-    rewrite count_occ_cons_eq in H5. rewrite count_occ_cons_neq in H5.
-    rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
-    rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
-    rewrite <- H5 in H9.
-    rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
-    rewrite <- Nat.add_0_r in H9 at 1. rewrite <- Nat.add_assoc in H9.
-    rewrite Nat.add_cancel_l in H9. inversion H9.
-    easy. reflexivity. reflexivity. easy.
-    reflexivity.
-
-    rewrite app_assoc_reverse. apply app_inv_head_iff.
-    rewrite app_assoc_reverse. rewrite app_assoc_reverse.
-    rewrite app_assoc_reverse. rewrite app_assoc_reverse.
-    apply app_inv_head_iff. apply app_inv_head_iff.
-    rewrite app_assoc_reverse.
-    apply app_inv_head_iff. apply app_inv_head_iff.
-    rewrite app_assoc_reverse.
-    reflexivity.
-
-    reflexivity.
+    + reflexivity.
+    + rewrite count_occ_app in H9. rewrite count_occ_app in H9.
+      rewrite count_occ_cons_eq in H9. rewrite count_occ_cons_neq in H9.
+      rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
+      rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
+      rewrite count_occ_app in H5. rewrite count_occ_app in H5.
+      rewrite count_occ_cons_neq in H5. rewrite count_occ_cons_eq in H5.
+      rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
+      rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
+      rewrite H5 in H9.
+      rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
+      rewrite <- Nat.add_0_r in H9. rewrite <- Nat.add_assoc in H9.
+      rewrite Nat.add_cancel_l in H9. inversion H9.
+      reflexivity. easy. easy. reflexivity.
+    + rewrite count_occ_app in H9. rewrite count_occ_app in H9.
+      rewrite count_occ_cons_neq in H9. rewrite count_occ_cons_eq in H9.
+      rewrite count_occ_nil in H9. rewrite count_occ_nil in H9.
+      rewrite Nat.add_1_r in H9. rewrite Nat.add_0_r in H9.
+      rewrite count_occ_app in H5. rewrite count_occ_app in H5.
+      rewrite count_occ_cons_eq in H5. rewrite count_occ_cons_neq in H5.
+      rewrite count_occ_nil in H5. rewrite count_occ_nil in H5.
+      rewrite Nat.add_1_r in H5. rewrite Nat.add_0_r in H5.
+      rewrite <- H5 in H9.
+      rewrite <- Nat.add_1_r in H9. rewrite <- Nat.add_1_r in H9.
+      rewrite <- Nat.add_0_r in H9 at 1. rewrite <- Nat.add_assoc in H9.
+      rewrite Nat.add_cancel_l in H9. inversion H9.
+      easy. reflexivity. reflexivity. easy.
+    + reflexivity.
+    + rewrite app_assoc_reverse. apply app_inv_head_iff.
+      rewrite app_assoc_reverse. rewrite app_assoc_reverse.
+      rewrite app_assoc_reverse. rewrite app_assoc_reverse.
+      apply app_inv_head_iff. apply app_inv_head_iff.
+      rewrite app_assoc_reverse.
+      apply app_inv_head_iff. apply app_inv_head_iff.
+      rewrite app_assoc_reverse.
+      reflexivity.
+    + reflexivity.
 Qed.