X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_sle_isi.ma;h=e05bd2a3f99bf48aae88f45ef6a8ded2bc983d1e;hb=742e21da086654af82f308027250d00b50d67f52;hp=ffe97e69f106c857991bca4601da721d4a6a2028;hpb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_isi.ma
index ffe97e69f..e05bd2a3f 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_isi.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_sle.ma".
 
 (*** sle_isid_sn *)
 corec lemma pr_sle_isi_sn:
-            ∀f1. 𝐈❪f1❫ → ∀f2. f1 ⊆ f2.
+            ∀f1. 𝐈❨f1❩ → ∀f2. f1 ⊆ f2.
 #f1 * -f1
 #f1 #g1 #Hf1 #H1 #f2 cases (pr_map_split_tl f2) *
 /3 width=5 by pr_sle_weak, pr_sle_push/
@@ -31,7 +31,7 @@ qed.
 
 (*** sle_inv_isid_dx *)
 corec lemma pr_sle_inv_isi_dx:
-            ∀f1,f2. f1 ⊆ f2 → 𝐈❪f2❫ → 𝐈❪f1❫.
+            ∀f1,f2. f1 ⊆ f2 → 𝐈❨f2❩ → 𝐈❨f1❩.
 #f1 #f2 * -f1 -f2
 #f1 #f2 #g1 #g2 #Hf * * #H
 [2,3: elim (pr_isi_inv_next … H) // ]