diff --git a/thue-morse.v b/thue-morse.v
index b0eec01..ebfcc62 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -786,8 +786,7 @@ Proof.
   induction n.
   - reflexivity.
   - simpl. replace (tm_morphism (tm_step n)) with (tm_step (S n)).
-    rewrite IHn. simpl. reflexivity.
-    simpl. reflexivity.
+    rewrite IHn. reflexivity. reflexivity.
 Qed.
 
 Lemma tm_step_end_2 : forall (n : nat),
@@ -831,7 +830,7 @@ Proof.
   rewrite tm_build.
   rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.sub_diag.
   replace (true) with (negb false). apply map_nth_error.
-  rewrite tm_step_head_1. simpl. reflexivity.
+  rewrite tm_step_head_1. reflexivity.
   reflexivity. rewrite tm_size_power2. easy.
 Qed.
 
@@ -845,7 +844,7 @@ Proof.
   rewrite tm_size_power2. rewrite <- Nat.sub_succ_l.
   rewrite Nat.sub_succ. rewrite Nat.sub_0_r.
   rewrite Nat.sub_diag. rewrite tm_step_end_1.
-  simpl. reflexivity.
+  reflexivity.
 
   rewrite Nat.le_succ_l. induction n. simpl. apply Nat.lt_0_1.
   rewrite Nat.mul_lt_mono_pos_r with (p := 2) in IHn.
@@ -1201,7 +1200,7 @@ Proof.
   intros n m k j. intros H I.
 
   assert (L: nth_error (tm_step m) 0 = Some false).
-  rewrite tm_step_head_1. simpl. reflexivity.
+  rewrite tm_step_head_1. reflexivity.
 
   assert (M: 2^j < 2^m).
   apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.