update in ground, static_2 and 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 1db92adaeaa4ed12e21b44a6dd321309552d048e..48c57a284d5c40be84a66789ed560a8cf5392c97 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 → 𝐈❨f❩.
+lemma pr_uni_isi (f): ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89\90 f → 𝐈❨f❩.
 /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© â\86\92 ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89¡ f.
+lemma pr_isi_inv_uni (f): ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90®â\9d¨ð\9d\9f\8eâ\9d© â\89\90 f.
 /2 width=1 by pr_isi_inv_eq_id/ qed-.