X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flfprs_lfpxs.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flfprs_lfpxs.ma;h=8c8679a475f0159e3af37f42569e2058da066e06;hb=d4ab51c20dbccd1e88cd2c4dcdaf3b4e56301155;hp=0000000000000000000000000000000000000000;hpb=d1bd9d230123f4045e2472d073c5dc4b5da30b34;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_lfpxs.ma
new file mode 100644
index 000000000..8c8679a47
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_lfpxs.ma
@@ -0,0 +1,3 @@
+(* Basic_2A1: was just: lprs_lpxs *)
+lemma lprs_lfpxs: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2.
+/3 width=3 by lpr_lpx, monotonic_TC/ qed.