From 99a4a193b6ea608b605400b31b39e74ef71cfd81 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 23 Nov 2022 21:27:09 +0100 Subject: [PATCH] Update --- thue-morse.v | 5 ----- 1 file changed, 5 deletions(-) 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.