X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flfpxs_etc.ma;h=e70a8f5969640836f6c540c60f65b3f0341174a6;hb=b0eb62e60a2fd73ba39c7a0df112f04131528602;hp=05f1e7357074d8c951efca0349737f012bc9ce72;hpb=c9b2cad6a92aedba63318319169d057251b2d138;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma
index 05f1e7357..e70a8f596 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma
@@ -8,7 +8,7 @@ lemma lfpxs_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G).
 #h #G #L1 #T1 #T2 #HT12 #L2 #H
 elim (tc_lfxs_inv_lex_lfeq … H) -H #L #HL1 #HL2
 lapply (lfxs_lex … HL1 T1) #H
-elim (cpx_lfxs_conf_gen … HT12 … H) -HT12 -H // #_ #HT21 #_
+elim (cpx_lfxs_conf_fle … HT12 … H) -HT12 -H // #_ #HT21 #_
 @(lfpxs_lpxs_lfeq … HL1) -HL1
 @(fle_lfxs_trans … HL2) //
 qed-.