- advances on 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
deleted file mode 100644 (file)
index 8c8679a..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma
+++ /dev/null
@@ -1,3 +0,0 @@
-(* 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.