X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbg.ma;h=696fee8ef78dbc23ac7387b64c7369c19eb44e16;hb=c7b50fec51b9a25d5bc536f44e54179fd53efb44;hp=2c2f375f2bc141e0607f445ddb2f08fdbb584c8b;hpb=f308429a0fde273605a2330efc63268b4ac36c99;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
index 2c2f375f2..696fee8ef 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
@@ -39,7 +39,7 @@ lemma fpbg_fpbq_trans: ∀h,G1,G,G2,L1,L,L2,T1,T,T2.
 qed-.
 
 lemma fpbg_fqu_trans (h): ∀G1,G,G2,L1,L,L2,T1,T,T2.
-                          ⦃G1,L1,T1⦄ >[h] ⦃G,L,T⦄ → ⦃G,L,T⦄ ⊐ ⦃G2,L2,T2⦄ →
+                          ⦃G1,L1,T1⦄ >[h] ⦃G,L,T⦄ → ⦃G,L,T⦄ ⬂ ⦃G2,L2,T2⦄ →
                           ⦃G1,L1,T1⦄ >[h] ⦃G2,L2,T2⦄.
 #h #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2
 /4 width=5 by fpbg_fpbq_trans, fpbq_fquq, fqu_fquq/
@@ -52,13 +52,13 @@ lemma fpbg_fpbs_trans: ∀h,G,G2,L,L2,T,T2. ⦃G,L,T⦄ ≥[h] ⦃G2,L2,T2⦄ 
 qed-.
 
 (* Basic_2A1: uses: fpbg_fleq_trans *)
-lemma fpbg_fdeq_trans: ∀h,G1,G,L1,L,T1,T. ⦃G1,L1,T1⦄ >[h] ⦃G,L,T⦄ →
+lemma fpbg_feqx_trans: ∀h,G1,G,L1,L,T1,T. ⦃G1,L1,T1⦄ >[h] ⦃G,L,T⦄ →
                        ∀G2,L2,T2. ⦃G,L,T⦄ ≛ ⦃G2,L2,T2⦄ → ⦃G1,L1,T1⦄ >[h] ⦃G2,L2,T2⦄.
-/3 width=5 by fpbg_fpbq_trans, fpbq_fdeq/ qed-.
+/3 width=5 by fpbg_fpbq_trans, fpbq_feqx/ qed-.
 
 (* Properties with t-bound rt-transition for terms **************************)
 
-lemma cpm_tdneq_cpm_fpbg (h) (G) (L):
+lemma cpm_tneqx_cpm_fpbg (h) (G) (L):
                          ∀n1,T1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → (T1 ≛ T → ⊥) →
                          ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → ⦃G,L,T1⦄ >[h] ⦃G,L,T2⦄.
-/4 width=5 by fpbq_fpbs, cpm_fpbq, cpm_fpb, ex2_3_intro/ qed. 
+/4 width=5 by fpbq_fpbs, cpm_fpbq, cpm_fpb, ex2_3_intro/ qed.