update in static_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 b610f09586a981a271454aaa4ecd7fbebecc2f85..4f811399e0f50ae5e53bb67c70db2a02316a603e 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.â\93\93(â\93\9dW.V), L2 = K0.â\93\93W, T0 = #0, T1 = â¬\86*[1]V *)
+(* Note: Take L0 = K0.â\93\93(â\93\9dW.V), L2 = K0.â\93\93W, T0 = #0, T1 = â\87§*[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⦄.