X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Ffqus.ma;h=c05bb114531e3e1dec56a3ebbb38eea74628e196;hb=e5378812c068074f0ac627541d3f066e135c8824;hp=325be4b397a4aff7c24d7e24480a4d46d074ccad;hpb=928cfe1ebf2fbd31731c8851cdec70802596016d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma
index 325be4b39..c05bb1145 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma
@@ -56,7 +56,7 @@ lemma fqus_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L,
 /2 width=5 by tri_TC_strap/ qed-.
 
 lemma fqus_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ →
-                  ∀L1,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
+                  ∀L1,U1,e. ⇩[e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
                   ⦃G1, L1, U1⦄ ⊃* ⦃G2, K2, T2⦄.
 #G1 #G2 #K1 #K2 #T1 #T2 #H @(fqus_ind … H) -G2 -K2 -T2
 /3 width=5 by fqus_strap1, fquq_fqus, fquq_drop/