X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Frpx_fsle.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Frpx_fsle.ma;h=5eed0ea7acd240a7b6be802ec8d73af0d928b509;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=d7e5e89ea11d5b3bd6059a0a5edcb0978c082c58;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

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 d7e5e89ea..5eed0ea7a 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
@@ -22,12 +22,12 @@ 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: "❨L2, T1❩ ⊆ ❨L2, T0❩" does not hold *)
 (* Note: Take L0 = K0.ⓓ(ⓝW.V), L2 = K0.ⓓW, T0 = #0, T1 = ⇧[1]V *)
 (* Note: This invalidates rpxs_cpx_conf: "∀G. s_r_confluent1 … (cpx G) (rpxs G)" *)
 lemma rpx_cpx_conf_fsge (G):
-      ∀L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈ T1 →
-      ∀L2. ❪G,L0❫ ⊢⬈[T0] L2 → ❪L2,T1❫ ⊆ ❪L0,T0❫.
+      ∀L0,T0,T1. ❨G,L0❩ ⊢ T0 ⬈ T1 →
+      ∀L2. ❨G,L0❩ ⊢⬈[T0] L2 → ❨L2,T1❩ ⊆ ❨L0,T0❩.
 #G0 #L0 #T0 @(fqup_wf_ind_eq (Ⓣ) … G0 L0 T0) -G0 -L0 -T0
 #G #L #T #IH #G0 #L0 * *
 [ #s0 #HG #HL #HT #X #HX #Y #HY destruct -IH
@@ -135,6 +135,6 @@ lemma rpx_cpx_conf_sn (G): s_r_confluent1 … (cpx G) (rpx G).
 /2 width=5 by cpx_rex_conf_sn/ qed-.
 
 lemma rpx_cpx_conf_fsge_dx (G):
-      ∀L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈ T1 →
-      ∀L2. ❪G,L0❫ ⊢⬈[T0] L2 → ❪L2,T1❫ ⊆ ❪L0,T1❫.
+      ∀L0,T0,T1. ❨G,L0❩ ⊢ T0 ⬈ T1 →
+      ∀L2. ❨G,L0❩ ⊢⬈[T0] L2 → ❨L2,T1❩ ⊆ ❨L0,T1❩.
 /3 width=5 by rpx_cpx_conf_sn, rpx_fsge_comp/ qed-.