update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / cnv_acle.ma

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 4a4a015ac134014113f2699cc9dfaaf3dfe65bc0..c0ad6880a720b9df254539d0ed74cf6e3847dad4 100644 (file)
--- 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 â\8a\86 a2 â\86\92 â\88\80G,L,T. â¦\83G,Lâ¦\84 â\8a¢ T ![h,a1] â\86\92 â¦\83G,Lâ¦\84 ⊢ T ![h,a2].
+      a1 â\8a\86 a2 â\86\92 â\88\80G,L,T. â\9dªG,Lâ\9d« â\8a¢ T ![h,a1] â\86\92 â\9dªG,Lâ\9d« ⊢ 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):
-      â\88\80G,L,T. â¦\83G,Lâ¦\84 â\8a¢ T ![h,a] â\86\92 â¦\83G,Lâ¦\84 ⊢ T ![h,𝛚].
+      â\88\80G,L,T. â\9dªG,Lâ\9d« â\8a¢ T ![h,a] â\86\92 â\9dªG,Lâ\9d« ⊢ T ![h,𝛚].
 /3 width=3 by cnv_acle_trans, acle_omega/ qed-.
 
 lemma cnv_acle_one (h) (a) (n):
-      â\88\80G,L,T. â¦\83G,Lâ¦\84 â\8a¢ T ![h,ð\9d\9f\8f] â\86\92 ad a n â\86\92 â¦\83G,Lâ¦\84 ⊢ T ![h,a].
+      â\88\80G,L,T. â\9dªG,Lâ\9d« â\8a¢ T ![h,ð\9d\9f\8f] â\86\92 ad a n â\86\92 â\9dªG,Lâ\9d« ⊢ T ![h,a].
 /3 width=3 by cnv_acle_trans, acle_one/ qed-.