X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flsubsx_lfsx.ma;h=059cb1ece177dee1167068ee30d3f8c145d34bd2;hp=4ef9cf96238e41a1c213148fc011d42563e6c2fe;hb=e8971d3db8935436e6dddc27fe1ae168c7f3b315;hpb=47a745462a714af9d65cea7b61af56524bd98fa1

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma
index 4ef9cf962..059cb1ece 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma
@@ -62,3 +62,12 @@ qed-.
 lemma lfsx_cpx_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
                       G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
 /3 width=6 by lfsx_cpx_trans_lsubsx, lsubsx_refl/ qed-.
+
+(* Properties with strong normalizing env's for uncounted rt-computation ****)
+
+lemma lfsx_cpxs_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
+                       G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
+#h #o #G #L #T1 #T2 #H
+@(cpxs_ind_dx ???????? H) -T1 //
+/3 width=3 by lfsx_cpx_trans/
+qed-.