diff --git a/thue-morse.v b/thue-morse.v
index 9800b77..cf6f0c3 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -942,6 +942,76 @@ Proof.
   rewrite tm_size_power2. apply Nat.le_add_l.
 Qed.
 
+Require Import Ltac2.Option.
+Lemma tm_step_next_range2_flip_two : forall (n k m : nat),
+  k < 2^n -> m < 2^n ->
+    nth_error (tm_step n) k = nth_error (tm_step n) m
+    <->
+    nth_error (tm_step (S n)) (k + 2^n)
+      = nth_error (tm_step (S n)) (m + 2^n).
+Proof.
+  intros n k m. intros H. intros I.
+  (* Part 1: preamble *)
+
+  assert (nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n)).
+  generalize H. apply tm_step_next_range2.
+  assert (nth_error (tm_step n) m <> nth_error (tm_step (S n)) (m + 2^n)).
+  generalize I. apply tm_step_next_range2.
+
+  assert (K: k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
+  generalize H. apply Nat.add_lt_mono_r.
+  assert (J: m + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
+  generalize I. apply Nat.add_lt_mono_r.
+
+  (* Part 2 *)
+  assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
+  generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
+  assert (nth_error (tm_step n) m = Some (nth m (tm_step n) false)).
+  generalize I. rewrite <- tm_size_power2. apply nth_error_nth'.
+  assert (nth_error (tm_step (S n)) (k + 2 ^ n) =
+    Some (nth (k + 2^n) (tm_step (S n)) false)).
+  generalize K. rewrite <- tm_size_power2. rewrite <- tm_size_power2.
+  apply nth_error_nth'.
+  assert (nth_error (tm_step (S n)) (m + 2 ^ n) =
+    Some (nth (m + 2^n) (tm_step (S n)) false)).
+  generalize J. rewrite <- tm_size_power2. rewrite <- tm_size_power2.
+  apply nth_error_nth'.
+  rewrite H2. rewrite H3. rewrite H4. rewrite H5.
+
+  (* Part 3 *)
+  destruct (nth k (tm_step n) false).
+  destruct (nth m (tm_step n) false).
+  destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
+  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
+  easy.
+  rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
+  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
+  rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
+  easy.
+  destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
+  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
+  rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
+  easy.
+  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
+  easy.
+  rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
+  destruct (nth m (tm_step n) false).
+  destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
+  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
+  rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
+  easy.
+  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
+  easy.
+  rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
+  destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
+  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
+  easy.
+  rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
+  destruct (nth (m + 2 ^ n) (tm_step (S n)) false).
+  rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
+  easy.
+Qed.
+
 Lemma tm_step_next_range2_neighbor : forall (n k : nat),
   S k < 2^n ->
     nth_error (tm_step n) k = nth_error (tm_step n) (S k)
@@ -1101,19 +1171,13 @@ Proof.
   apply Nat.lt_succ_diag_r.
   generalize H1. generalize H0. apply Nat.lt_trans. rewrite <- H1.
   rewrite tm_step_repunit_index. destruct (odd n). easy. easy.
+  rewrite <- J. rewrite I.
 
   (*
   assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
   apply tm_step_repunit.
    *)
   
-Lemma tm_step_next_range :
-  forall (n k : nat) (b : bool),
-  nth_error (tm_step n) k = Some b -> nth_error (tm_step (S n)) k = Some b.
-Theorem tm_step_stable : forall (n m k : nat),
-  k < 2^n -> k < 2^m -> nth_error(tm_step n) k = nth_error (tm_step m) k.
-
-