λδ-2B is released

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma
index b8e919b738cc635d1b8cd26a6ecddc9666468845..adeaa3f882be30565e34efa719b754c6c7dd9e91 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma
@@ -27,7 +27,7 @@ lemma jsx_csx_conf (h) (G):
 
 (* Properties with strongly rt-normalizing referred local environments ******)
 
-(* Note: Try by induction on the 2nd premise by generalizing V with f *) 
+(* Note: Try by induction on the 2nd premise by generalizing V with f *)
 lemma rsx_jsx_trans (h) (G):
       ∀L1,V. G ⊢ ⬈*[h,V] 𝐒⦃L1⦄ →
       ∀L2. G ⊢ L1 ⊒[h] L2 → G ⊢ ⬈*[h,V] 𝐒⦃L2⦄.