X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbs_cpx.ma;h=c3cdaf038300adf182435d7c6f27a4c9ad6ba15e;hb=222044da28742b24584549ba86b1805a87def070;hp=3acf1a16861da0d494db3eff8082446348329a51;hpb=f129bbbfda0e65a5f92ec086246f6e288376d4f9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma
index 3acf1a168..c3cdaf038 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/rt_transition/cpx_ffdeq.ma".
+include "basic_2/rt_transition/cpx_fdeq.ma".
 include "basic_2/rt_computation/lpxs_cpxs.ma".
 include "basic_2/rt_computation/fpbs_lpxs.ma".
 
@@ -26,8 +26,8 @@ lemma fpbs_cpx_tdneq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o]
                             ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ≥[h, o] ⦃G2, L2, U2⦄.
 #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2
 elim (fpbs_inv_star … H) -H #G0 #L0 #L3 #T0 #T3 #HT10 #H10 #HL03 #H32
-elim (ffdeq_cpx_trans … H32 … HTU2) -HTU2 #T4 #HT34 #H42
-lapply (ffdeq_tdneq_repl_dx … H32 … H42 … HnTU2) -T2 #HnT34
+elim (fdeq_cpx_trans … H32 … HTU2) -HTU2 #T4 #HT34 #H42
+lapply (fdeq_tdneq_repl_dx … H32 … H42 … HnTU2) -T2 #HnT34
 lapply (lpxs_cpx_trans … HT34 … HL03) -HT34 #HT34
 elim (fqus_cpxs_trans_tdneq … H10 … HT34 HnT34) -T3 #T2 #HT02 #HnT02 #H24
 elim (tdeq_dec h o T1 T0) [ #H10 | -HnT02 #HnT10 ]