X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Frpx_fsle.ma;h=3bce5e5cc2f917ddc5284e08cba87f214835c018;hp=29c6a5cd3de00374b4b48d5f291c924ef426cf7c;hb=25c634037771dff0138e5e8e3d4378183ff49b86;hpb=bd53c4e895203eb049e75434f638f26b5a161a2b

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma
index 29c6a5cd3..3bce5e5cc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma
@@ -23,7 +23,7 @@ include "basic_2/rt_transition/rpx_fqup.ma".
 (* Forward lemmas with free variables inclusion for restricted closures *****)
 
 (* Note: "❪L2, T1❫ ⊆ ❪L2, T0❫" does not hold *)
-(* Note: Take L0 = K0.ⓓ(ⓝW.V), L2 = K0.ⓓW, T0 = #0, T1 = ⇧*[1]V *)
+(* Note: Take L0 = K0.ⓓ(ⓝW.V), L2 = K0.ⓓW, T0 = #0, T1 = ⇧[1]V *)
 (* Note: This invalidates rpxs_cpx_conf: "∀h, G. s_r_confluent1 … (cpx h G) (rpxs h G)" *)
 lemma rpx_cpx_conf_fsge (h) (G): ∀L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈[h] T1 →
                                  ∀L2. ❪G,L0❫ ⊢⬈[h,T0] L2 → ❪L2,T1❫ ⊆ ❪L0,T0❫.