X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_isu_uni.ma;h=bb4cceedea88d5cc9dcc40a319573e43e5964484;hb=b1c5b3370653db6e495bbf6b3799cba592746cdd;hp=7ff9c2e57f6862dbaf9427416824a2ee8d60eb68;hpb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;p=helm.git

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 7ff9c2e57..bb4cceede 100644
--- 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): 𝐔❪𝐮❨n❩❫.
+lemma pr_isu_uni (n): 𝐔❨𝐮❨n❩❩.
 #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): 𝐔❪f❫ → ∃n. 𝐮❨n❩ ≡ f.
+lemma pr_isu_inv_uni (f): 𝐔❨f❩ → ∃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/