X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpxs_lfpx.ma;h=73cee45379ef37200a9daf6c01581ffed6c27f85;hb=a0462cc68401e561a041f1e567dec40cd522cab8;hp=66196f7262b0dcb9afe4da6abe055c914a9f25f3;hpb=aed322a0e2db2c8248281582e324ef09cd732421;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma
index 66196f726..73cee4537 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/rt_transition/lfpx_fqup.ma".
-include "basic_2/rt_transition/lfpx_lfpx.ma".
+include "basic_2/rt_transition/lfpx_cpx.ma".
 include "basic_2/rt_computation/cpxs_drops.ma".
 include "basic_2/rt_computation/cpxs_cpxs.ma".
 
@@ -30,8 +30,8 @@ lemma lfpx_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpx h G).
 | #I #G #L2 #V #V2 #W2 #_ #IH #HVW2 #Y1 #H
   elim (lfpx_inv_zero_pair_dx … H) -H #L1 #V1 #HL1 #HV1 #H destruct
   /5 width=3 by lfpx_cpx_conf, cpxs_delta, cpxs_strap2/
-| #I #G #L2 #V #V2 #W2 #i #_ #IH #HVW2 #Y1 #H
-  elim (lfpx_inv_lref_pair_dx … H) -H #L1 #V1 #HL1 #HV1
+| #I2 #G #L2 #V2 #W2 #i #_ #IH #HVW2 #Y1 #H
+  elim (lfpx_inv_lref_bind_dx … H) -H #I1 #L1 #HL1 #H destruct
   /4 width=3 by cpxs_lref, cpxs_strap2/
 | #p #I #G #L2 #V #V2 #T #T2 #_ #_ #IHV #IHT #L1 #H
   elim (lfpx_inv_bind … H) -H /3 width=1 by cpxs_bind/