X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_sdj_isi.ma;h=b1e4650b96ec53c686334a42f3ad0f8e7f1d4c5e;hb=61bc42e04598a9f5e489c3867af72e700c7fda04;hp=f8a94240950aceeb2cfacad81bacbae709b6fa87;hpb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sdj_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sdj_isi.ma
index f8a942409..b1e4650b9 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sdj_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sdj_isi.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_sdj.ma".
 
 (*** sdj_isid_dx *)
 corec lemma pr_sdj_isi_dx:
-            ∀f2. 𝐈❪f2❫ → ∀f1. f1 ∥ f2.
+            ∀f2. 𝐈❨f2❩ → ∀f1. f1 ∥ f2.
 #f2 * -f2
 #f2 #g2 #Hf2 #H2 #f1 cases (pr_map_split_tl f1) *
 /3 width=5 by pr_sdj_next_push, pr_sdj_push_bi/
@@ -29,7 +29,7 @@ qed.
 
 (*** sdj_isid_sn *)
 corec lemma pr_sdj_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_sdj_push_next, pr_sdj_push_bi/
@@ -39,7 +39,7 @@ qed.
 
 (*** sdj_inv_refl *)
 corec lemma pr_sdj_inv_refl:
-            ∀f. f ∥ f →  𝐈❪f❫.
+            ∀f. f ∥ f →  𝐈❨f❩.
 #f cases (pr_map_split_tl f) #Hf #H
 [ lapply (pr_sdj_inv_push_bi … H … Hf Hf) -H /3 width=3 by pr_isi_push/
 | elim (pr_sdj_inv_next_bi … H … Hf Hf)