diff --git a/thue-morse.v b/thue-morse.v
index fcdc5bb..e1cec88 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -23,15 +23,6 @@ Fixpoint tm_step (n: nat) : list bool :=
   end.
 
 (* ad hoc more or less general lemmas *)
-Lemma negb_map_explode : forall (l1 l2 : list bool),
-  map negb (l1 ++ l2) = map negb l1 ++ map negb l2.
-Proof.
-  intros l1 l2.
-  induction l1.
-  - reflexivity.
-  - simpl. rewrite IHl1. reflexivity.
-Qed.
-
 Lemma negb_double_map : forall (l : list bool),
   map negb (map negb l) = l.
 Proof.
@@ -117,7 +108,7 @@ Lemma tm_morphism_rev : forall (l : list bool),
 Proof.
   intro l. induction l.
   - reflexivity.
-  - simpl. rewrite negb_map_explode.
+  - simpl. rewrite map_app.
     rewrite IHl. rewrite tm_morphism_concat.
     rewrite <- app_assoc. simpl.
     rewrite negb_involutive. reflexivity.
@@ -306,7 +297,7 @@ Proof.
   - reflexivity.
   - simpl. rewrite tm_step_lemma. rewrite IHn. rewrite tm_morphism_concat.
     simpl in IHn. rewrite IHn. rewrite tm_build_negb. rewrite IHn.
-    rewrite negb_map_explode. rewrite negb_double_map.
+    rewrite map_app. rewrite negb_double_map.
     reflexivity.
 Qed.