X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_coafter_ist_isi.ma;h=53f51deaf013975461701d3fb66c737a71eb3d62;hb=d06053844638d88936d711b66fddbcca2a9add1c;hp=50a68b5fbfa1bc65b58438bf42619ba283b4c0a5;hpb=8ec019202bff90959cf1a7158b309e7f83fa222e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma
index 50a68b5fb..53f51deaf 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma
@@ -27,7 +27,7 @@ definition H_pr_coafter_des_ist_sn_isi: predicate pr_map ≝
 
 (*** coafter_fwd_isid2_O_aux *)
 corec fact pr_coafter_des_ist_sn_isi_unit_aux:
-           ∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1.
+           ∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1.
 #f1 #H1f1 #f2 #f #H #H2f1 #Hf
 cases (pr_pat_inv_unit_bi … H1f1) -H1f1 [ |*: // ] #g1 #H1
 lapply (pr_ist_inv_push … H2f1 … H1) -H2f1 #H2g1
@@ -42,8 +42,8 @@ qed-.
 
 (*** coafter_fwd_isid2_aux *)
 fact pr_coafter_des_ist_sn_isi_aux:
-     (∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1) →
-     ∀i2,f1. @❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_sn_isi f1.
+     (∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1) →
+     ∀i2,f1. ＠⧣❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_sn_isi f1.
 #H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
 #i2 #IH #f1 #H1f1 #f2 #f #H #H2f1 #Hf
 elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1