λδ-2B is released

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
index 31ebb2c771013868994633d252550d2ea7fc482b..d162f660a984b37fbadc4e8b274881d8207ed719 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
@@ -98,6 +98,6 @@ lemma csx_fwd_flat: ∀h,I,G,L,V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓕ{I}V.T⦄ 
             sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind
 *)
 (* Basic_2A1: removed theorems 6:
-              csxa_ind csxa_intro csxa_cpxs_trans csxa_intro_cpx 
+              csxa_ind csxa_intro csxa_cpxs_trans csxa_intro_cpx
               csx_csxa csxa_csx
 *)