X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fldrop_leq.ma;h=75586d3d3b5b27ae8b826af9cc898fb6ffb09709;hb=3325b784763ae9e6bac4307463071bb38e5641c9;hp=91b20e72029387b813b2bd7d4c04553def7c5d5a;hpb=a0d25627e80a3a2fe68da954b68f6d541c6dbc34;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma
index 91b20e720..75586d3d3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma
@@ -63,7 +63,7 @@ lemma ldrop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i →
                    ∃∃L2. L1 ≃[0, i] L2 & ⇩[i] L2 ≡ K2.
 #K2 #i @(nat_ind_plus … i) -i
 [ /3 width=3 by leq_O2, ex2_intro/
-| #i #IHi #Y #Hi elim (ldrop_O1_lt Y 0) //
+| #i #IHi #Y #Hi elim (ldrop_O1_lt (Ⓕ) Y 0) //
   #I #L1 #V #H lapply (ldrop_inv_O2 … H) -H #H destruct
   normalize in Hi; elim (IHi L1) -IHi
   /3 width=5 by ldrop_drop, leq_pair, injective_plus_l, ex2_intro/