update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_uni.ma
index 122b8433ef4edc607e6f9e305802adf69ee62544..1db92adaeaa4ed12e21b44a6dd321309552d048e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_uni.ma
@@ -20,11 +20,11 @@ include "ground/relocation/pr_isi_id.ma".
 (* Constructions with pr_isi ************************************************)
 
 (*** uni_inv_isid uni_isi *)
-lemma pr_uni_isi (f): ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89¡ f â\86\92 ð\9d\90\88â\9dªfâ\9d«.
+lemma pr_uni_isi (f): ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89¡ f â\86\92 ð\9d\90\88â\9d¨fâ\9d©.
 /2 width=1 by pr_eq_id_isi/ qed.
 
 (* Inversions with pr_isi ***************************************************)
 
 (*** uni_isid isi_inv_uni *)
-lemma pr_isi_inv_uni (f): ð\9d\90\88â\9dªfâ\9d« → 𝐮❨𝟎❩ ≡ f.
+lemma pr_isi_inv_uni (f): ð\9d\90\88â\9d¨fâ\9d© → 𝐮❨𝟎❩ ≡ f.
 /2 width=1 by pr_isi_inv_eq_id/ qed-.