diff --git a/thue-morse.v b/thue-morse.v
index 174b9c2..da526ce 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1036,7 +1036,6 @@ Proof.
       generalize K. generalize J. apply tm_step_stable.
 
       rewrite <- H2 in H1. rewrite H0 in H1. inversion H1.
-      replace (tm_morphism (tm_step (n + m))) with (tm_step (S n + m)) in H4.
       rewrite H4.
 
       assert (nth_error (tm_step n) (S k) = Some(nth (S k) (tm_step n) false)).
@@ -1070,10 +1069,6 @@ Proof.
       rewrite H3 in H6. rewrite H5 in H6.
       inversion H6. rewrite H8.
 
-      replace (tm_morphism (tm_step (n + m))) with (tm_step (S n + m)).
-      reflexivity.
-
-      reflexivity.
       reflexivity.
 Qed.