Update

2023-01-04 17:58:57 +01:00 · 2023-01-04 17:58:57 +01:00 · c2f9b2a0d5
commit c2f9b2a0d5
parent 13152cd05c
1 changed files with 2 additions and 3 deletions
--- 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),