X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_nat_nat.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_nat_nat.ma;h=481ff1517b32ba7b414dd34db594ea48217ab985;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=5f40670806d0b94279bcd3e47540f9178acccce9;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_nat.ma
index 5f4067080..481ff1517 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_nat.ma
@@ -20,7 +20,7 @@ include "ground/relocation/pr_nat.ma".
 (* Main destructions ********************************************************)
 
 theorem pr_nat_monotonic (k2) (l2) (f):
-        @↑❪l2,f❫ ≘ k2 → ∀k1,l1. @↑❪l1,f❫ ≘ k1 → l1 < l2 → k1 < k2.
+        @↑❨l2,f❩ ≘ k2 → ∀k1,l1. @↑❨l1,f❩ ≘ k1 → l1 < l2 → k1 < k2.
 #k2 @(nat_ind_succ … k2) -k2
 [ #l2 #f #H2f elim (pr_nat_inv_zero_dx … H2f) -H2f //
   #g #H21 #_ #k1 #l1 #_ #Hi destruct
@@ -37,7 +37,7 @@ theorem pr_nat_monotonic (k2) (l2) (f):
 qed-.
 
 theorem pr_nat_inv_monotonic (k1) (l1) (f):
-        @↑❪l1,f❫ ≘ k1 → ∀k2,l2. @↑❪l2,f❫ ≘ k2 → k1 < k2 → l1 < l2.
+        @↑❨l1,f❩ ≘ k1 → ∀k2,l2. @↑❨l2,f❩ ≘ k2 → k1 < k2 → l1 < l2.
 #k1 @(nat_ind_succ … k1) -k1
 [ #l1 #f #H1f elim (pr_nat_inv_zero_dx … H1f) -H1f //
   #g * -l1 #H #k2 #l2 #H2f #Hk
@@ -59,14 +59,14 @@ theorem pr_nat_inv_monotonic (k1) (l1) (f):
 qed-.
 
 theorem pr_nat_mono (f) (l) (l1) (l2):
-        @↑❪l,f❫ ≘ l1 → @↑❪l,f❫ ≘ l2 → l2 = l1.
+        @↑❨l,f❩ ≘ l1 → @↑❨l,f❩ ≘ l2 → l2 = l1.
 #f #l #l1 #l2 #H1 #H2 elim (nat_split_lt_eq_gt l2 l1) //
 #Hi elim (nlt_ge_false l l)
 /2 width=6 by pr_nat_inv_monotonic/
 qed-.
 
 theorem pr_nat_inj (f) (l1) (l2) (l):
-        @↑❪l1,f❫ ≘ l → @↑❪l2,f❫ ≘ l → l1 = l2.
+        @↑❨l1,f❩ ≘ l → @↑❨l2,f❩ ≘ l → l1 = l2.
 #f #l1 #l2 #l #H1 #H2 elim (nat_split_lt_eq_gt l2 l1) //
 #Hi elim (nlt_ge_false l l)
 /2 width=6 by pr_nat_monotonic/