X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fsteps%2Frtc_plus.ma;h=87adfee3a41afd50db73bfe58b730dc1c5f58b88;hb=b6e1db4f1b0f1d5121f2b214562f96c5b0fa544e;hp=900e6b4836e6f0ce739d3d2927ec1b35e1aa1882;hpb=0e2836b432e8d1a10262836e160a5dd3cfb82c1e;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 900e6b483..87adfee3a 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
@@ -27,10 +27,11 @@ interpretation "plus (rtc)"
 
 (* Basic properties *********************************************************)
 
-lemma plus_rew: ∀ri1,ri2,rs1,rs2,ti1,ti2,ts1,ts2. 
-                〈ri1+ri2, rs1+rs2, ti1+ti2, ts1+ts2〉 =
-                plus (〈ri1,rs1,ti1,ts1〉) (〈ri2,rs2,ti2,ts2〉).
-// qed. (**) (* disambiguation of plus fails *)
+(**) (* plus is not disambiguated parentheses *) 
+lemma plus_rew: ∀ri1,ri2,rs1,rs2,ti1,ti2,ts1,ts2.
+                 〈ri1+ri2, rs1+rs2, ti1+ti2, ts1+ts2〉 =
+                 (〈ri1,rs1,ti1,ts1〉) + (〈ri2,rs2,ti2,ts2〉).
+// qed.
 
 lemma plus_O_dx: ∀c. c = c + 𝟘𝟘.
 * #ri #rs #ti #ts <plus_rew //