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=8f1a123e61ff079b1f9ad63cc915470ec7e6abf3;hp=1e6706a8bb8207db4234aaadab22f7a110c384e6;hpb=11093619476326238c2ef9d2dfe9150b8c9bc920;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 1e6706a8b..bb4cceede 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma
@@ -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/