X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Ftrace_at.ma;h=02d8ac1ebae0cc17fa5cbcb1c6530362bf181d08;hb=a8cd6cc85182245df447a21caf16b6503fa4b3e5;hp=0fd397829a58fea5ce1ccd2eec2b2facbe3930cf;hpb=46815bb7af06b235ead2fd67a4aee2d294b51928;p=helm.git

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 0fd397829..02d8ac1eb 100644
--- 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-.