- advances on lfxs for lfpxs

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / lfpxs_etc.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma
new file mode 100644 (file)
index 0000000..8c8679a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.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.