notational update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_id.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_id.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_id.ma
index c08e32055de35e02ccb1916ff3a47f14a407dfa5..0c63147efa39ece95b02e44997ce55228da12a29 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_id.ma
@@ -24,8 +24,8 @@ lemma id_isid: 𝐈⦃𝐈𝐝⦄.
 
 (* Alternative definition of isid *******************************************)
 
-lemma eq_id_isid: â\88\80f. ð\9d\90\88ð\9d\90\9d â\89\97 f → 𝐈⦃f⦄.
+lemma eq_id_isid: â\88\80f. ð\9d\90\88ð\9d\90\9d â\89¡ f → 𝐈⦃f⦄.
 /2 width=3 by isid_eq_repl_back/ qed.
 
-lemma eq_id_inv_isid: â\88\80f. ð\9d\90\88â¦\83fâ¦\84 â\86\92 ð\9d\90\88ð\9d\90\9d â\89\97 f.
+lemma eq_id_inv_isid: â\88\80f. ð\9d\90\88â¦\83fâ¦\84 â\86\92 ð\9d\90\88ð\9d\90\9d â\89¡ f.
 /2 width=1 by isid_inv_eq_repl/ qed-.