update in ground, static_2 and apps_2

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_isi_id.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_id.ma
index 374fcdce4d5dfd2befc46b08ecf901ba365ab1f2..9e3ffed0968acc3d7c5c2621773989aee50b38d0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_id.ma
@@ -26,9 +26,9 @@ lemma pr_isi_id: 𝐈❨𝐢❩.
 (* Alternative definition with pr_id and pr_eq ******************************)
 
 (*** eq_id_isid *)
-lemma pr_eq_id_isi (f): ð\9d\90¢ â\89¡ f → 𝐈❨f❩.
+lemma pr_eq_id_isi (f): ð\9d\90¢ â\89\90 f → 𝐈❨f❩.
 /2 width=3 by pr_isi_eq_repl_back/ qed.
 
 (*** eq_id_inv_isid *)
-lemma pr_isi_inv_eq_id (f): ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90¢ â\89¡ f.
+lemma pr_isi_inv_eq_id (f): ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90¢ â\89\90 f.
 /2 width=1 by pr_isi_inv_eq_repl/ qed-.