X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fpnat_plus.ma;h=af5bd09432c8b3460d1d5123d9c0f3ecd56bb819;hp=8096e849ba554d7164c90362c3897d1b395591fd;hb=0bcf2dc1a27e38cb6cd3d44eb838d652926841e0;hpb=7e120a2bf2e6c0882b4f4b376c5861e001945cf4

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index 8096e849b..af5bd0943 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
@@ -25,7 +25,7 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma pplus_one_dx (p): ↑p = p + 𝟏.
+lemma pplus_unit_dx (p): ↑p = p + 𝟏.
 // qed.
 
 lemma pplus_succ_dx (p) (q): ↑(p+q) = p + ↑q.
@@ -37,7 +37,7 @@ lemma pplus_succ_sn (p) (q): ↑(p+q) = ↑p + q.
 #p #q @(piter_appl … psucc)
 qed.
 
-lemma pplus_one_sn (p): ↑p = 𝟏 + p.
+lemma pplus_unit_sn (p): ↑p = 𝟏 + p.
 #p elim p -p //
 qed.
 
@@ -54,7 +54,7 @@ qed.
 
 lemma eq_inv_unit_pplus (p) (q): 𝟏 = p + q → ⊥.
 #p #q elim q -q
-[ <pplus_one_dx #H destruct
+[ <pplus_unit_dx #H destruct
 | #q #_ <pplus_succ_dx #H destruct
 ]
 qed-.