]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma
update in ground static_2 basic_2 apps_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / jsx_csx.ma
index c11a6bfc9e8e47a71c607cfc6c69bf21959be22d..82137a8e559bf75ebb1fe336b5ae5ab8855d0410 100644 (file)
@@ -22,7 +22,7 @@ include "basic_2/rt_computation/jsx_lsubr.ma".
 
 lemma jsx_csx_conf (G):
       ∀L1,L2. G ⊢ L1 ⊒ L2 →
-      â\88\80T. â\9dªG,L1â\9d« â\8a¢ â¬\88\9d\90\92 T â\86\92 â\9dªG,L2â\9d« ⊢ ⬈*𝐒 T.
+      â\88\80T. â\9d¨G,L1â\9d© â\8a¢ â¬\88\9d\90\92 T â\86\92 â\9d¨G,L2â\9d© ⊢ ⬈*𝐒 T.
 /3 width=5 by jsx_fwd_lsubr, csx_lsubr_conf/ qed-.
 
 (* Properties with strongly rt-normalizing referred local environments ******)