From db1b42ac8c3bd4952a728443fb425f02319fcef4 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Sat, 14 Jan 2023 20:31:22 +0100 Subject: [PATCH] Update --- src/thue_morse.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/thue_morse.v b/src/thue_morse.v index 94b7551..cbc9a91 100644 --- a/src/thue_morse.v +++ b/src/thue_morse.v @@ -413,7 +413,7 @@ Proof. apply tm_step_count_occ. rewrite count_occ_app in L. rewrite count_occ_app in L. rewrite K in L. rewrite Nat.add_cancel_l in L. - destruct b. simpl in L. inversion L. simpl in L. inversion L. + destruct b; simpl in L; inversion L. Qed. Lemma tm_step_consecutive_identical' :