X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Flfpxs%2Flfpxs_cpxs.etc;h=a6eb3b6ac334e72fc462ea177147759a584107dd;hb=58ea181757dce19b875b2f5a224fe193b2263004;hp=6edda23e14449d5cf2d45e21ea2fa2d491c375a4;hpb=670ad7822d59e598a38d9037d482d3de188b170c;p=helm.git

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 6edda23e1..a6eb3b6ac 100644
--- 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.
-