X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_to_mono%2Ftrace_alphabet.ma;h=52c91909d8aef47b10e7c451189acb2229313ec8;hb=ab0d181f9a89f461a9c280f42a949a2dc2abe44c;hp=2c162745f6e31d9d900275351f81a598c31e524c;hpb=31790e8f6fa051f710f41e4c17d67701874ba331;p=helm.git

diff --git a/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma b/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma
index 2c162745f..52c91909d 100644
--- a/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma
+++ b/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma
@@ -252,7 +252,7 @@ lemma to_blank_cons_nb: ∀sig,n,i,a,l.
 qed.
 
 axiom to_blank_hd : ∀sig,n,a,b,l1,l2. 
-  (∀i. i ≤ n → to_blank_i sig n i (a::l1) = to_blank_i sig n i (b::l2)) → a = b.
+  (∀i. i < n → to_blank_i sig n i (a::l1) = to_blank_i sig n i (b::l2)) → a = b.
 
 lemma to_blank_i_ext : ∀sig,n,i,l.
   to_blank_i sig n i l = to_blank_i sig n i (l@[all_blanks …]).