X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fsteps%2Frtc_plus.ma;h=41f0e8a273e59ffc1875150bcb2311110cb1649c;hb=c3904c007394068ed823575e3be3d73a9ad92cce;hp=75a58b25f55b0abc1b7a8e4fc5280c139b0e927f;hpb=fb246e36bb7d2731016e686e2091f6a3704bb362;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
index 75a58b25f..41f0e8a27 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
@@ -24,3 +24,13 @@ definition plus (r1:rtc) (r2:rtc): rtc ≝ match r1 with [
 
 interpretation "plus (rtc)"
    'plus r1 r2 = (plus r1 r2).
+
+(* Basic properties *********************************************************)
+
+lemma plus_OO_r: ∀r. r = 𝟘𝟘 + r.
+* normalize //
+qed.
+
+lemma plus_r_OO: ∀r. r = r + 𝟘𝟘.
+* normalize //
+qed.