λδ-2B is released

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma
index 06500ddc957c4e009eaaf67a08f519164eb90708..2671597f13eca7211c17021b3b598766fd8f0b56 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma
@@ -63,7 +63,7 @@ qed-.
 lemma rsx_fwd_flat_dx (h) (G):
       ∀I,L,V,T. G ⊢ ⬈*[h,ⓕ{I}V.T] 𝐒⦃L⦄ →
       G ⊢ ⬈*[h,T] 𝐒⦃L⦄.
-#h #G #I #L #V #T #H 
+#h #G #I #L #V #T #H
 @(rsx_ind … H) -L #L1 #_ #IHL1
 @rsx_intro #L2 #HL12 #HnL12
 /4 width=3 by reqx_fwd_flat_dx/