X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_ist_isi.ma;h=87485963ea6c6bfc9341ca23d3cc7aa6ad7f3a4f;hb=8f1a123e61ff079b1f9ad63cc915470ec7e6abf3;hp=ce24651dadada833d98953afcb025c6d28430a3c;hpb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_isi.ma
index ce24651da..87485963e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_isi.ma
@@ -20,7 +20,7 @@ include "ground/relocation/pr_ist.ma".
 (* Advanced constructions with pr_isi ***************************************)
 
 (*** isid_at_total *)
-lemma pr_isi_pat_total: ∀f. 𝐓❪f❫ → (∀i1,i2. @❪i1,f❫ ≘ i2 → i1 = i2) → 𝐈❪f❫.
+lemma pr_isi_pat_total: ∀f. 𝐓❨f❩ → (∀i1,i2. ＠⧣❨i1,f❩ ≘ i2 → i1 = i2) → 𝐈❨f❩.
 #f #H1f #H2f @pr_isi_pat
 #i lapply (H1f i) -H1f *
 #j #Hf >(H2f … Hf) in ⊢ (???%); -H2f //