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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpx.ma
index ac7a93d62..d8b2c1390 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpx.ma
@@ -22,5 +22,5 @@ include "basic_2/rt_transition/lpr.ma".
 
 (* Basic_2A1: was: lpr_lpx *)
 lemma lpr_fwd_lpx (h) (G):
-      ∀L1,L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L1❫ ⊢ ⬈ L2.
+      ∀L1,L2. ❨G,L1❩ ⊢ ➡[h,0] L2 → ❨G,L1❩ ⊢ ⬈ L2.
 /3 width=3 by cpm_fwd_cpx, lex_co/ qed-.