- revision of ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cpx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
index 6de953b282e14d98196466ed44069b0cda0d88e4..840bf0866c06eb991a1f43207a72fb7cb299ca7b 100644 (file)
--- 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/