X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Flleq_fqus.ma;h=28bb175edeeffa790cd2f8696a96795a802f21d1;hb=c60524dec7ace912c416a90d6b926bee8553250b;hp=eea2d3486a062949ab44c946758c3bc9a81a7c8a;hpb=f10cfe417b6b8ec1c7ac85c6ecf5fb1b3fdf37db;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_fqus.ma
index eea2d3486..28bb175ed 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_fqus.ma
@@ -35,8 +35,8 @@ lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐ ⦃G2, K2, U⦄ 
   #H3 #H4 /2 width=3 by fqu_bind_dx, ex2_intro/
 | #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H
   /2 width=3 by fqu_flat_dx, ex2_intro/
-| #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12
-  elim (drop_O1_le (Ⓕ) (e+1) L1)
+| #G #L2 #K2 #T #U #m #HLK2 #HTU #L1 #HL12
+  elim (drop_O1_le (Ⓕ) (m+1) L1)
   [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/
   | lapply (drop_fwd_length_le2 … HLK2) -K2
     lapply (lleq_fwd_length … HL12) -T -U //