X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_coafter_ist_isf.ma;h=9c522c5bae9aaf2e11c1c2142e344d289b6f25d4;hb=ad6182251b8192ee7d25c53156afbce35e3715b6;hp=c3f81859245cae750bf053c908b6749980abf542;hpb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isf.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isf.ma
index c3f818592..9c522c5ba 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isf.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isf.ma
@@ -22,13 +22,13 @@ include "ground/relocation/pr_coafter_isi.ma".
 
 (*** H_coafter_isfin2_fwd *)
 definition H_pr_coafter_des_ist_isf: predicate pr_map ≝
-           λf1. ∀f2. 𝐅❪f2❫ → 𝐓❪f1❫ → ∀f. f1 ~⊚ f2 ≘ f →  𝐅❪f❫.
+           λf1. ∀f2. 𝐅❨f2❩ → 𝐓❨f1❩ → ∀f. f1 ~⊚ f2 ≘ f →  𝐅❨f❩.
 
 (* Destructions with pr_ist and pr_isf **************************************)
 
 (*** coafter_isfin2_fwd_O_aux *)
 fact pr_coafter_des_ist_isf_unit_aux:
-     ∀f1. @❪𝟏, f1❫ ≘ 𝟏 → H_pr_coafter_des_ist_isf f1.
+     ∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_isf f1.
 #f1 #Hf1 #f2 #H
 generalize in match Hf1; generalize in match f1; -f1
 @(pr_isf_ind … H) -f2
@@ -44,8 +44,8 @@ qed-.
 
 (*** coafter_isfin2_fwd_aux *)
 fact pr_coafter_des_ist_isf_aux:
-     (∀f1. @❪𝟏, f1❫ ≘ 𝟏 → H_pr_coafter_des_ist_isf f1) →
-     ∀i2,f1. @❪𝟏, f1❫ ≘ i2 → H_pr_coafter_des_ist_isf f1.
+     (∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_isf f1) →
+     ∀i2,f1. ＠⧣❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_isf f1.
 #H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
 #i2 #IH #f1 #H1f1 #f2 #Hf2 #H2f1 #f #Hf
 elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1