update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_conversion / cpc_cpc.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc_cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc_cpc.ma
index d3151122a0bf9560eece7f5c586535f4488fc208..49528eac8856d442894649f8a0a37ad79e81368c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc_cpc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc_cpc.ma
@@ -18,6 +18,6 @@ include "basic_2/rt_conversion/cpc.ma".
 
 (* Main properties **********************************************************)
 
-theorem cpc_conf: â\88\80h,G,L,T0,T1,T2. â¦\83G,Lâ¦\84 â\8a¢ T0 â¬\8c[h] T1 â\86\92 â¦\83G,Lâ¦\84 ⊢ T0 ⬌[h] T2 →
-                  â\88\83â\88\83T. â¦\83G,Lâ¦\84 â\8a¢ T1 â¬\8c[h] T & â¦\83G,Lâ¦\84 ⊢ T2 ⬌[h] T.
+theorem cpc_conf: â\88\80h,G,L,T0,T1,T2. â\9dªG,Lâ\9d« â\8a¢ T0 â¬\8c[h] T1 â\86\92 â\9dªG,Lâ\9d« ⊢ T0 ⬌[h] T2 →
+                  â\88\83â\88\83T. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\8c[h] T & â\9dªG,Lâ\9d« ⊢ T2 ⬌[h] T.
 /3 width=3 by cpc_sym, ex2_intro/ qed-.