X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flfpxs_cpxs.ma;h=e5e5ea562c03fe170303f81cfaaa6d60fd885864;hb=6555775aa5268dec0d9ae4579412b659cacdc964;hp=e565bdc6760bce3a70789419767d65c57ed5f02f;hpb=69592aa1d0c0d122fb09f11cc53bf4c5a1532fdd;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma
index e565bdc67..e5e5ea562 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma
@@ -72,7 +72,7 @@ lemma cpxs_inv_abbr1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈*[h] U2
     /4 width=3 by lfpxs_pair, cpxs_trans, ex3_intro, or_intror/
   ]
 | #U1 #HTU1 #HU01
-  elim (cpx_lifts … HU02 (Ⓣ) … (L.ⓓV1) … HU01)
+  elim (cpx_lifts_sn … HU02 (Ⓣ) … (L.ⓓV1) … HU01)
   /4 width=3 by cpxs_strap1, drops_refl, drops_drop, ex3_intro, or_intror/
 ]
 qed-.