X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcpx.ma;h=840bf0866c06eb991a1f43207a72fb7cb299ca7b;hb=658c000ee2ea2da04cf29efc0acdaf16364fbf5e;hp=6de953b282e14d98196466ed44069b0cda0d88e4;hpb=1994fe8e6355243652770f53a02db5fdf26915f0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
index 6de953b28..840bf0866 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
@@ -82,7 +82,7 @@ lemma cpx_delift: ∀h,g,I,G,K,V,T1,L,l. ⬇[l] L ≡ (K.ⓑ{I}V) →
                   ∃∃T2,T.  ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 & ⬆[l, 1] T ≡ T2.
 #h #g #I #G #K #V #T1 elim T1 -T1
 [ * #i #L #l /2 width=4 by cpx_atom, lift_sort, lift_gref, ex2_2_intro/
-  elim (lt_or_eq_or_gt i l) #Hil [1,3: /3 width=4 by cpx_atom, lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ ]
+  elim (lt_or_eq_or_gt i l) #Hil [1,3: /4 width=4 by cpx_atom, lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ]
   destruct
   elim (lift_total V 0 (i+1)) #W #HVW
   elim (lift_split … HVW i i) /3 width=7 by cpx_delta, ex2_2_intro/