diff --git a/src/thue_morse.v b/src/thue_morse.v
index 736d8fd..15d7c6c 100644
--- a/src/thue_morse.v
+++ b/src/thue_morse.v
@@ -292,9 +292,8 @@ Theorem tm_step_negb : forall (n : nat),
 Proof.
   intro n.
   rewrite <- tm_step_lemma. symmetry.
-  replace (tm_step n) with (rev (rev (tm_step n))); rewrite rev_involutive.
-  - rewrite tm_morphism_rev. rewrite tm_build_negb. reflexivity.
-  - reflexivity.
+  rewrite tm_morphism_rev. rewrite tm_build_negb. rewrite rev_involutive.
+  reflexivity.
 Qed.
 
 Theorem tm_build : forall (n : nat),