X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcsx_lift.ma;h=4f06e7912938bf49280b8e7a83e40af1636a0f6f;hb=e5378812c068074f0ac627541d3f066e135c8824;hp=5194bedfe8608992ec038876dd64a33d440c4c9b;hpb=928cfe1ebf2fbd31731c8851cdec70802596016d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
index 5194bedfe..4f06e7912 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
@@ -48,7 +48,7 @@ lemma csx_inv_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V →
                          ⦃G, L⦄ ⊢ ⬊*[h, g] #i → ⦃G, K⦄ ⊢ ⬊*[h, g] V.
 #h #g #I #G #L #K #V #i #HLK #Hi
 elim (lift_total V 0 (i+1))
-/4 width=9 by csx_inv_lift, csx_cpx_trans, cpx_delta, ldrop_fwd_ldrop2/
+/4 width=9 by csx_inv_lift, csx_cpx_trans, cpx_delta, ldrop_fwd_drop2/
 qed-.
 
 (* Advanced properties ******************************************************)
@@ -61,7 +61,7 @@ elim (cpx_inv_lref1 … H) -H
 [ #H destruct elim Hi //
 | -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1
   lapply (ldrop_mono … HLK0 … HLK) -HLK #H destruct
-  /3 width=7 by csx_lift, csx_cpx_trans, ldrop_fwd_ldrop2/
+  /3 width=7 by csx_lift, csx_cpx_trans, ldrop_fwd_drop2/
 ]
 qed.