X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_acle.ma;h=c0ad6880a720b9df254539d0ed74cf6e3847dad4;hp=4a4a015ac134014113f2699cc9dfaaf3dfe65bc0;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_acle.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_acle.ma
index 4a4a015ac..c0ad6880a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_acle.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_acle.ma
@@ -20,7 +20,7 @@ include "basic_2/dynamic/cnv_aaa.ma".
 (* Properties with preorder for applicability domains ***********************)
 
 lemma cnv_acle_trans (h) (a1) (a2):
-      a1 ⊆ a2 → ∀G,L,T. ⦃G,L⦄ ⊢ T ![h,a1] → ⦃G,L⦄ ⊢ T ![h,a2].
+      a1 ⊆ a2 → ∀G,L,T. ❪G,L❫ ⊢ T ![h,a1] → ❪G,L❫ ⊢ T ![h,a2].
 #h #a1 #a2 #Ha12 #G #L #T #H elim H -G -L -T
 [ /1 width=1 by cnv_sort/
 | /3 width=1 by cnv_zero/
@@ -34,9 +34,9 @@ lemma cnv_acle_trans (h) (a1) (a2):
 qed-.
 
 lemma cnv_acle_omega (h) (a):
-      ∀G,L,T. ⦃G,L⦄ ⊢ T ![h,a] → ⦃G,L⦄ ⊢ T ![h,𝛚].
+      ∀G,L,T. ❪G,L❫ ⊢ T ![h,a] → ❪G,L❫ ⊢ T ![h,𝛚].
 /3 width=3 by cnv_acle_trans, acle_omega/ qed-.
 
 lemma cnv_acle_one (h) (a) (n):
-      ∀G,L,T. ⦃G,L⦄ ⊢ T ![h,𝟏] → ad a n → ⦃G,L⦄ ⊢ T ![h,a].
+      ∀G,L,T. ❪G,L❫ ⊢ T ![h,𝟏] → ad a n → ❪G,L❫ ⊢ T ![h,a].
 /3 width=3 by cnv_acle_trans, acle_one/ qed-.