X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_pat_lt.ma;h=5fe0250c10bc94b2b9855941dbac7e5ff40bb89e;hb=77479649510792efe4d9cbff508e118360862594;hp=c58c16172803d1778b22ce7b889956149d39d3e4;hpb=9b4e20442ec5a4028cfe2b6fe836c94acdb033b8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_lt.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_lt.ma
index c58c16172..5fe0250c1 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_lt.ma
@@ -22,7 +22,7 @@ include "ground/relocation/pr_pat.ma".
 
 (*** at_increasing *)
 lemma pr_pat_increasing (i2) (i1) (f):
-      @❨i1,f❩ ≘ i2 → i1 ≤ i2.
+      ＠⧣❨i1,f❩ ≘ i2 → i1 ≤ i2.
 #i2 elim i2 -i2
 [ #i1 #f #Hf elim (pr_pat_inv_unit_dx … Hf) -Hf //
 | #i2 #IH * //
@@ -33,14 +33,14 @@ qed-.
 
 (*** at_increasing_strict *)
 lemma pr_pat_increasing_strict (g) (i1) (i2):
-      @❨i1,g❩ ≘ i2 → ∀f. ↑f = g →
-      ∧∧ i1 < i2 & @❨i1,f❩ ≘ ↓i2.
+      ＠⧣❨i1,g❩ ≘ i2 → ∀f. ↑f = g →
+      ∧∧ i1 < i2 & ＠⧣❨i1,f❩ ≘ ↓i2.
 #g #i1 #i2 #Hg #f #H elim (pr_pat_inv_next … Hg … H) -Hg -H
 /4 width=2 by conj, pr_pat_increasing, ple_succ_bi/
 qed-.
 
 (*** at_fwd_id_ex *)
-lemma pr_pat_des_id (f) (i): @❨i,f❩ ≘ i → ⫯⫰f = f.
+lemma pr_pat_des_id (f) (i): ＠⧣❨i,f❩ ≘ i → ⫯⫰f = f.
 #f elim (pr_map_split_tl f) //
 #H #i #Hf elim (pr_pat_inv_next … Hf … H) -Hf -H
 #j2 #Hg #H destruct lapply (pr_pat_increasing … Hg) -Hg
@@ -51,8 +51,8 @@ qed-.
 
 (*** at_le_ex *)
 lemma pr_pat_le_ex (j2) (i2) (f):
-      @❨i2,f❩ ≘ j2 → ∀i1. i1 ≤ i2 →
-      ∃∃j1. @❨i1,f❩ ≘ j1 & j1 ≤ j2.
+      ＠⧣❨i2,f❩ ≘ j2 → ∀i1. i1 ≤ i2 →
+      ∃∃j1. ＠⧣❨i1,f❩ ≘ j1 & j1 ≤ j2.
 #j2 elim j2 -j2 [2: #j2 #IH ] #i2 #f #Hf
 [ elim (pr_pat_inv_succ_dx … Hf) -Hf [1,3: * |*: // ]
   #g [ #x2 ] #Hg [ #H2 ] #H0
@@ -71,7 +71,7 @@ qed-.
 
 (*** at_id_le *)
 lemma pr_pat_id_le (i1) (i2):
-      i1 ≤ i2 → ∀f. @❨i2,f❩ ≘ i2 → @❨i1,f❩ ≘ i1.
+      i1 ≤ i2 → ∀f. ＠⧣❨i2,f❩ ≘ i2 → ＠⧣❨i1,f❩ ≘ i1.
 #i1 #i2 #H
 @(ple_ind_alt … H) -i1 -i2 [ #i2 | #i1 #i2 #_ #IH ] #f #Hf
 lapply (pr_pat_des_id … Hf) #H <H in Hf; -H