]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_cpmuwe.ma
update in ground_2, static_2, basic_2, apps_2, alpha_1
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cpmuwe_cpmuwe.ma
index deea7cdd4f9149f0b6aa3d1f5f2673b4fb1ea5bb..3ebd3c366f67c7b84a454b79e16c4ea6ab9931a9 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. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] -â\93\93V.U â\86\92 â¦\83G,Lâ¦\84 ⊢ T ➡*𝐍𝐖*[h,n] -ⓓV.U.
+      â\88\80V,U. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] -â\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. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] â\93\9b{p}W.U â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*ð\9d\90\8dð\9d\90\96*[h,n] â\93\9b{p}W.U.
+      â\88\80W,U. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] â\93\9b[p]W.U â\86\92 â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*ð\9d\90\8dð\9d\90\96*[h,n] â\93\9b[p]W.U.
 /3 width=5 by cnuw_abst, cpmuwe_intro/ qed.