update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / list_rcons.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
index 322235e7a15cc326f44a5c4d9c5873851f1a5612..00faad83dc2af5462773b9ef7ba0fc592ed623c1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
@@ -40,7 +40,7 @@ lemma list_append_rcons_sn (A):
 // qed.
 
 lemma list_append_rcons_dx (A):
-      ∀l1,l2,a. l1 ⨁ l2 ⨭ a = l1 ⨁{A} (l2 ⨭ a).
+      ∀l1,l2,a. (l1 ⨁ l2) ⨭ a = l1 ⨁{A} (l2 ⨭ a).
 // qed.
 
 (* Basic inversions *********************************************************)