Update

src/thue_morse2.v

@@ -189,27 +189,29 @@ Lemma tm_step_factor5' : forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ tl -> length a = 5
   -> a <> [ false; true; false; true; false].
 Proof.
-
-
-
-
-
-
-
-
-  assert ({last (b :: hd) true = true} + {last (b :: hd) true <> true}).
-  apply bool_dec.
-  assert (last (b::hd) true = true). destruct H1. assumption.
-  apply not_true_is_false in n0.
-
-  replace ((removelast (b :: hd) ++ [last (b :: hd) true]) ++ a ++ tl)
-    with ((removelast (b :: hd)) ++ [false;true] ++ [false;true]
-                                 ++ [false;true] ++ tl) in H.
-  apply tm_step_cubefree in H. contradiction H. reflexivity.
-  simpl. apply Nat.lt_0_2.
+  intros n hd a tl. intros H I.
+  assert (K: {a=[false; true; false; true; false]}
+           + {~ a=[false; true; false; true; false]}).
+  apply list_eq_dec. apply bool_dec. destruct K.
+  assert (tm_step (S n) = hd ++ a ++ tl
+          ++ (map negb hd) ++ [ true; false; true; false; true ]
+          ++ (map negb tl)).
+  rewrite tm_build. rewrite H.
+  rewrite map_app. rewrite map_app.
   rewrite <- app_assoc. apply app_inv_head_iff.
-  rewrite n0. rewrite e. reflexivity.
-  rewrite H1 in H.
+  rewrite <- app_assoc. rewrite e. reflexivity.
+  rewrite app_assoc in H0. rewrite app_assoc in H0.
+  rewrite app_assoc in H0. apply tm_step_factor5 in H0.
+  contradiction H0. reflexivity.
+  reflexivity. assumption.
+Qed.
+
+
+
+
+
+
+