Update

2023-01-04 18:19:26 +01:00 · 2023-01-04 18:19:26 +01:00 · e946fefe47
commit e946fefe47
parent f3aa7478fb
1 changed files with 1 additions and 2 deletions
--- a/src/thue_morse.v
+++ b/src/thue_morse.v
@ -1347,8 +1347,7 @@ Proof.
    assert (J: exists (hd a tl : list bool),
      tm_step n = hd ++ a ++ a ++ a ++ tl /\ 0 < length a).
    exists hd. exists a. exists tl. split; assumption.
-    apply tm_step_cube7 in J.
-    destruct J. destruct H0. destruct H0. destruct H0.
+    apply tm_step_cube7 in J. destruct J. destruct H0. destruct H0. destruct H0.
    assert (0 < 0). generalize H1. generalize H0. apply tm_step_cube2.
    apply Nat.lt_irrefl in H2. contradiction H2.
  - assumption.