- advances towards strong normalization

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / lfpxs_cpxs.ma

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 e565bdc6760bce3a70789419767d65c57ed5f02f..e5e5ea562c03fe170303f81cfaaa6d60fd885864 100644 (file)
--- 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-.