- lfpxs based on tc_lfxs

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / lfpxs / lfpxs_cpxs.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc
index 6edda23e14449d5cf2d45e21ea2fa2d491c375a4..a6eb3b6ac334e72fc462ea177147759a584107dd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc
@@ -25,4 +25,3 @@ lemma lpxs_ind_alt: ∀h,o,G. ∀R:relation lenv.
 lemma lpxs_pair2: ∀h,o,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 →
                   ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, o] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2.ⓑ{I}V2.
 /3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed.
-