advances on ldrop ....

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / ldrop_leq.ma

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 91b20e72029387b813b2bd7d4c04553def7c5d5a..75586d3d3b5b27ae8b826af9cc898fb6ffb09709 100644 (file)
--- 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/