update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / pnat_plus.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index 8096e849ba554d7164c90362c3897d1b395591fd..af5bd09432c8b3460d1d5123d9c0f3ecd56bb819 100644 (file)
--- 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-.