X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbg.ma;h=bda560f425b152f8674c39ce778c325599d94cf6;hb=9aa2722ff4aa7868ffd14e5a820cd6dc79e2c8a6;hp=de77a268fd6de912d131d9b4ba962636e94c07f8;hpb=afd4afa9489fa65019ad7cdc274e261f6993b871;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 de77a268f..bda560f42 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
@@ -45,6 +45,14 @@ lemma fpbg_fpbs_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2,
 qed-.
 
 (* Basic_2A1: uses: fpbg_fleq_trans *)
-lemma fpbg_ffdeq_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >[h, o] ⦃G, L, T⦄ →
-                        ∀G2,L2,T2. ⦃G, L, T⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
-/3 width=5 by fpbg_fpbq_trans, fpbq_ffdeq/ qed-.
+lemma fpbg_fdeq_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ >[h, o] ⦃G, L, T⦄ →
+                       ∀G2,L2,T2. ⦃G, L, T⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
+/3 width=5 by fpbg_fpbq_trans, fpbq_fdeq/ qed-.
+
+(* Properties with t-bound rt-transition for terms **************************)
+
+lemma cpm_tdneq_cpm_fpbg (h) (o) (G) (L):
+                         ∀n1,T1,T. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T → (T1 ≛[h,o] T → ⊥) →
+                         ∀n2,T2. ⦃G, L⦄ ⊢ T ➡[n2,h] T2 →
+                         ⦃G, L, T1⦄ >[h,o] ⦃G, L, T2⦄.
+/4 width=5 by fpbq_fpbs, cpm_fpbq, cpm_fpb, ex2_3_intro/ qed.