]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_cpmuwe.ma
update in ground static_2 basic_2 apps_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cpmuwe_cpmuwe.ma
index c1257d25201f7accdddb051a1a60ef81bad2b7dd..aa0c5a9f4b5067885791b2d2d5745f5e9c968cb0 100644 (file)
@@ -20,9 +20,9 @@ include "basic_2/rt_computation/cpmuwe.ma".
 (* Advanced properties ******************************************************)
 
 lemma cpmuwe_abbr_neg (h) (n) (G) (L) (T):
-      â\88\80V,U. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[h,n] -â\93\93V.U â\86\92 â\9dªG,Lâ\9d« ⊢ T ➡*𝐍𝐖*[h,n] -ⓓV.U.
+      â\88\80V,U. â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,n] -â\93\93V.U â\86\92 â\9d¨G,Lâ\9d© ⊢ T ➡*𝐍𝐖*[h,n] -ⓓV.U.
 /3 width=5 by cnuw_abbr_neg, cpmuwe_intro/ qed.
 
 lemma cpmuwe_abst (h) (n) (p) (G) (L) (T):
-      â\88\80W,U. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[h,n] â\93\9b[p]W.U â\86\92 â\9dªG,Lâ\9d« ⊢ T ➡*𝐍𝐖*[h,n] ⓛ[p]W.U.
+      â\88\80W,U. â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,n] â\93\9b[p]W.U â\86\92 â\9d¨G,Lâ\9d© ⊢ T ➡*𝐍𝐖*[h,n] ⓛ[p]W.U.
 /3 width=5 by cnuw_abst, cpmuwe_intro/ qed.