update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma
index 7ff9c2e57f6862dbaf9427416824a2ee8d60eb68..1e6706a8bb8207db4234aaadab22f7a110c384e6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma
@@ -20,7 +20,7 @@ include "ground/relocation/pr_isu.ma".
 (* Constructions with pr_uni ************************************************)
 
 (*** isuni_uni *)
-lemma pr_isu_uni (n): ð\9d\90\94â\9dªð\9d\90®â\9d¨nâ\9d©â\9d«.
+lemma pr_isu_uni (n): ð\9d\90\94â\9d¨ð\9d\90®â\9d¨nâ\9d©â\9d©.
 #n @(nat_ind_succ … n) -n
 /3 width=3 by pr_isu_isi, pr_isu_next/
 qed.
@@ -43,7 +43,7 @@ lemma pr_isu_eq_repl_fwd:
 (* Inversions with pr_uni ***************************************************)
 
 (*** uni_isuni *)
-lemma pr_isu_inv_uni (f): ð\9d\90\94â\9dªfâ\9d« → ∃n. 𝐮❨n❩ ≡ f.
+lemma pr_isu_inv_uni (f): ð\9d\90\94â\9d¨fâ\9d© → ∃n. 𝐮❨n❩ ≡ f.
 #f #H elim H -f
 [ /3 width=2 by pr_isi_inv_uni, ex_intro/
 | #f #_ #g #H * /3 width=6 by pr_eq_next, ex_intro/