X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcsx_lpx.ma;h=f8bf3c47576c99256e1163c1e75edc674eeaa9f1;hb=1ca3d131ce61d857ebf691169e85ddb81250fd4e;hp=d1211415a792b8c83215363d94a4c7235d963047;hpb=c713c14cb3c69b1e9a4c693aed382eedc04512c1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma
index d1211415a..f8bf3c475 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma
@@ -25,7 +25,7 @@ lemma csx_lpx_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
                     ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
 #h #g #G #L1 #L2 #HL12 #T #H @(csx_ind_alt … H) -T
 /4 width=3 by csx_intro, lpx_cpx_trans/
-qed.
+qed-.
 
 lemma csx_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
                 ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓛ{a}W.T.