X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fmr2_plus.ma;h=29c76eb3369b2ce8d83c17745dfa1a8b338982df;hp=07374a027d845560ef722c68452522cef322e845;hb=8fdf1af656038d0245eba64ff2531bbe94ce0e9e;hpb=77c9255de3c5f7780aeacd745703a1cc76328a68

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/mr2_plus.ma b/matita/matita/contribs/lambdadelta/ground/relocation/mr2_plus.ma
index 07374a027..29c76eb33 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/mr2_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/mr2_plus.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground/arith/nat_minus_plus.ma".
 include "ground/relocation/mr2.ma".
 
 (* MULTIPLE RELOCATION WITH PAIRS *******************************************)
@@ -26,7 +27,7 @@ interpretation "plus (multiple relocation with pairs)"
 
 (* Basic properties *********************************************************)
 
-lemma pluss_SO2: ∀l,m,cs. (❨l,m❩;cs) + 1 = ❨↑l,m❩;cs + 1.
+lemma pluss_SO2: ∀l,m,cs. ((❨l,m❩;cs) + 𝟏) = ❨↑l,m❩;cs + 𝟏.
 normalize // qed.
 
 (* Basic inversion lemmas ***************************************************)
@@ -41,6 +42,6 @@ lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = ❨l,m❩;cs2 →
 #i #l #m #cs2 *
 [ normalize #H destruct
 | #l1 #m1 #cs1 whd in ⊢ (??%?→?); #H destruct
-  <minus_plus_m_m /2 width=3 by ex2_intro/
+  <nminus_plus_sn_refl_sn /2 width=3 by ex2_intro/
 ]
 qed-.