X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_isi_uni.ma;h=48c57a284d5c40be84a66789ed560a8cf5392c97;hb=8f1a123e61ff079b1f9ad63cc915470ec7e6abf3;hp=1db92adaeaa4ed12e21b44a6dd321309552d048e;hpb=8ec019202bff90959cf1a7158b309e7f83fa222e;p=helm.git

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 1db92adae..48c57a284 100644
--- 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): 𝐮❨𝟎❩ ≡ f → 𝐈❨f❩.
+lemma pr_uni_isi (f): 𝐮❨𝟎❩ ≐ 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): 𝐈❨f❩ → 𝐮❨𝟎❩ ≡ f.
+lemma pr_isi_inv_uni (f): 𝐈❨f❩ → 𝐮❨𝟎❩ ≐ f.
 /2 width=1 by pr_isi_inv_eq_id/ qed-.