X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbg.ma;h=bda560f425b152f8674c39ce778c325599d94cf6;hp=e3232f7e1b74b66437d222c6e448e57401d63d37;hb=9aa2722ff4aa7868ffd14e5a820cd6dc79e2c8a6;hpb=19a25bf176255055193372554437729a6fa1894c

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 e3232f7e1..bda560f42 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
@@ -48,3 +48,11 @@ 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.