diff --git a/thue-morse.v b/thue-morse.v
index 10e950a..631a014 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -872,8 +872,6 @@ Proof.
   apply list_app_length_lt in H0. rewrite H1 in H0. apply H0.
 Qed.
 
-
-
 Lemma tm_step_next_range2 :
   forall (n : nat) (l1 l2 : list bool) (b : bool),
   tm_step n = l1 ++ b :: l2
@@ -905,6 +903,42 @@ Proof.
   rewrite tm_size_power2. apply Nat.le_add_l.
 Qed.
 
+Theorem tm_fullrange : forall (n m k : nat),
+  k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
+Proof.
+  intros n m k. rewrite <- tm_size_power2. intros.
+  induction n.
+  - destruct m. reflexivity. simpl in H. rewrite Nat.lt_1_r in H. rewrite H. 
+    replace (tm_step (S m)) with (false :: tl (tm_step (S m))). reflexivity.
+    symmetry. apply tm_step_head_1.
+  - induction m. simpl in H0. rewrite Nat.lt_1_r in H0. rewrite H0.
+    replace (tm_step (S n)) with (false :: tl (tm_step (S n))). reflexivity.
+    symmetry. apply tm_step_head_1.
+
+
+
+
+
+
+
+
+  - induction m. reflexivity. simpl in H. rewrite Nat.lt_1_r in H. rewrite H. 
+    replace (tm_step (S m)) with (false :: tl (tm_step (S m))). reflexivity.
+    symmetry. apply tm_step_head_1.
+  - induction m. simpl in H0. rewrite Nat.lt_1_r in H0. rewrite H0.
+    replace (tm_step (S n)) with (false :: tl (tm_step (S n))). reflexivity.
+    symmetry. apply tm_step_head_1.
+    replace (nth_error (tm_step m) k) with (nth_error (tm_step (S m)) k) in IHm.
+    apply IHm.
+
+
+nth_error_nth':
+  forall [A : Type] (l : list A) [n : nat] (d : A),
+  n < length l -> nth_error l n = Some (nth n l d)
+
+
+
+
 
 Lemma tm_step_consecutive_power2 :
   forall (n k : nat) (l1 l2 : list bool) (b1 b2 b1' b2': bool),