diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 294430a..f8d82ca 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1819,7 +1819,7 @@ Proof.
 Qed.
 
 
-Lemma tm_step_palindromic_power2_even :
+Lemma tm_step_palindromic_power2_even_alpha :
   forall (m n : nat) (hd a tl : list bool),
     tm_step n = hd ++ a ++ (rev a) ++ tl
     -> 6 < length a
@@ -1892,7 +1892,7 @@ Proof.
 Qed.
 
 
-Lemma tm_step_palindromic_power2_even' :
+Lemma tm_step_palindromic_power2_even_beta :
   forall (m n : nat) (hd a tl : list bool),
     tm_step n = hd ++ a ++ (rev a) ++ tl
     -> 6 < length a
@@ -1981,7 +1981,7 @@ Proof.
 Qed.
 
 
-Theorem xxx :
+Theorem tm_step_palindromic_power2_even :
   forall (m n : nat) (hd a tl : list bool),
     tm_step n = hd ++ a ++ (rev a) ++ tl
     -> 6 < length a
@@ -1992,7 +1992,7 @@ Proof.
   assert (E: length (hd ++ a) mod (2 ^ (pred (Nat.double m))) = 0
      \/ 2^6 <= length a).
   generalize J. generalize I. generalize H.
-  apply tm_step_palindromic_power2_even'.
+  apply tm_step_palindromic_power2_even_beta.
 
   destruct m. rewrite J in I. inversion I. inversion H1.
   destruct m. rewrite J in I. inversion I. inversion H1.
@@ -2011,7 +2011,7 @@ Proof.
     contradiction H8. apply Nat.lt_1_2.
   - intros n tl a I J hd H E. assert (E' := E).
     destruct E as [E0 | E1]. assumption.
-    rewrite tm_step_palindromic_power2_even with (n := n) (tl := tl).
+    rewrite tm_step_palindromic_power2_even_alpha with (n := n) (tl := tl).
     rewrite <- pred_Sn.
 
 
@@ -2090,7 +2090,7 @@ Proof.
     apply IHm with (n := n) (tl := tl').
     assumption. assumption. assumption.
     generalize Y. generalize Y'. generalize H.
-    apply tm_step_palindromic_power2_even'.
+    apply tm_step_palindromic_power2_even_beta.
     easy. reflexivity. reflexivity.
     assumption. assumption. assumption.
 Qed.