basic properties of cpr ...

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / steps / rtc_plus.ma

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 900e6b4836e6f0ce739d3d2927ec1b35e1aa1882..87adfee3a41afd50db73bfe58b730dc1c5f58b88 100644 (file)
--- 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 //