- matita: computed auto traces now include the "width" parameter

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / trace_at.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
index 0fd397829a58fea5ce1ccd2eec2b2facbe3930cf..02d8ac1ebae0cc17fa5cbcb1c6530362bf181d08 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
@@ -139,7 +139,7 @@ lemma at_inv_le: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 ≤ ∥cs∥ ∧ i2 
 #cs #i1 #i2 #_ * /3 width=1 by le_S_S, conj/ 
 qed-.
 
-lemma at_inv_gt1: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∥cs∥  < i1 → ⊥.
+lemma at_inv_gt1: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∥cs∥ < i1 → ⊥.
 #cs #i1 #i2 #H elim (at_inv_le … H) -H /2 width=4 by lt_le_false/
 qed-.