diff --git a/thue_morse.v b/thue_morse.v
index 8a3a41d..0d565b2 100644
--- a/thue_morse.v
+++ b/thue_morse.v
@@ -375,12 +375,11 @@ Proof.
   intro n.
   rewrite <- Nat.sub_1_r. rewrite <- tm_size_power2.
   rewrite nth_error_nth' with (d := false).
-  rewrite <- rev_nth. rewrite tm_step_end_1. simpl.
-  reflexivity.
-  rewrite tm_size_power2.
-  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
-  rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
-  rewrite tm_size_power2. apply Nat.pow_nonzero. easy.
+  - rewrite <- rev_nth. rewrite tm_step_end_1. simpl. reflexivity.
+    rewrite tm_size_power2.
+    rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+  - rewrite Nat.sub_1_r. apply Nat.lt_pred_l.
+    rewrite tm_size_power2. apply Nat.pow_nonzero. easy.
 Qed.