update in ground_2, static_2, basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / rpx_fsle.ma

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 29c6a5cd3de00374b4b48d5f291c924ef426cf7c..3bce5e5cc2f917ddc5284e08cba87f214835c018 100644 (file)
--- 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❫.