advances on ldrop ....

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / lleq_fqus.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma
index ac1329b4530767e88b9a6363e0bf40f095eff7b3..c54215e60149917f169fbed91d7558318a464413 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma
@@ -36,7 +36,7 @@ lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐ ⦃G2, K2, U⦄ 
 | #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 (ldrop_O1_le (e+1) L1)
+  elim (ldrop_O1_le (Ⓕ) (e+1) L1)
   [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/
   | lapply (ldrop_fwd_length_le2 … HLK2) -K2
     lapply (lleq_fwd_length … HL12) -T -U //