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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_uni.ma
index 8831312c6..114284805 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_uni.ma
@@ -21,12 +21,12 @@ include "ground/relocation/pr_nat_nat.ma".
 (* Constructions with pr_uni ************************************************)
 
 lemma pr_nat_uni (n) (l):
-      @↑❪l,𝐮❨n❩❫ ≘ l+n.
+      @↑❨l,𝐮❨n❩❩ ≘ l+n.
 /2 width=1 by pr_nat_pred_bi/
 qed.
 
 (* Inversions with pr_uni ***************************************************)
 
 lemma pr_nat_inv_uni (n) (l) (k):
-      @↑❪l,𝐮❨n❩❫ ≘ k → k = l+n.
+      @↑❨l,𝐮❨n❩❩ ≘ k → k = l+n.
 /2 width=4 by pr_nat_mono/ qed-.