many changes

[helm.git] / matita / matita / lib / turing / multi_to_mono / trace_alphabet.ma

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 2c162745f6e31d9d900275351f81a598c31e524c..52c91909d8aef47b10e7c451189acb2229313ec8 100644 (file)
--- 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 …]).