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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fqup.ma
index e98884c8b..9ef86a2c9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fqup.ma
@@ -24,19 +24,19 @@ lemma rpx_refl (G):
 /2 width=1 by rex_refl/ qed.
 
 lemma rpx_pair_refl (G):
-      ∀L,V1,V2. ❪G,L❫ ⊢ V1 ⬈ V2 →
-      ∀I,T. ❪G,L.ⓑ[I]V1❫ ⊢ ⬈[T] L.ⓑ[I]V2.
+      ∀L,V1,V2. ❨G,L❩ ⊢ V1 ⬈ V2 →
+      ∀I,T. ❨G,L.ⓑ[I]V1❩ ⊢ ⬈[T] L.ⓑ[I]V2.
 /2 width=1 by rex_pair_refl/ qed.
 
 (* Advanced inversion lemmas ************************************************)
 
 lemma rpx_inv_bind_void (G):
-      ∀p,I,L1,L2,V,T. ❪G,L1❫ ⊢ ⬈[ⓑ[p,I]V.T] L2 →
-      ∧∧ ❪G,L1❫ ⊢ ⬈[V] L2 & ❪G,L1.ⓧ❫ ⊢ ⬈[T] L2.ⓧ.
+      ∀p,I,L1,L2,V,T. ❨G,L1❩ ⊢ ⬈[ⓑ[p,I]V.T] L2 →
+      ∧∧ ❨G,L1❩ ⊢ ⬈[V] L2 & ❨G,L1.ⓧ❩ ⊢ ⬈[T] L2.ⓧ.
 /2 width=3 by rex_inv_bind_void/ qed-.
 
 (* Advanced forward lemmas **************************************************)
 
 lemma rpx_fwd_bind_dx_void (G):
-      ∀p,I,L1,L2,V,T. ❪G,L1❫ ⊢ ⬈[ⓑ[p,I]V.T] L2 → ❪G,L1.ⓧ❫ ⊢ ⬈[T] L2.ⓧ.
+      ∀p,I,L1,L2,V,T. ❨G,L1❩ ⊢ ⬈[ⓑ[p,I]V.T] L2 → ❨G,L1.ⓧ❩ ⊢ ⬈[T] L2.ⓧ.
 /2 width=4 by rex_fwd_bind_dx_void/ qed-.