X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Flist_rcons.ma;h=2cf2e23bf07f662e9563fc2e0dccb9274e1ff8d7;hb=12dc655b7f5321b33b93a310d53e23e60e090caa;hp=429a766fd1a3616bdaa18050455561d301004217;hpb=dd41efaab7f147d5673cc30a27d36375f9b52c9d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
index 429a766fd..2cf2e23bf 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
@@ -24,7 +24,7 @@ interpretation
 (* Basic constructions ******************************************************)
 
 lemma list_cons_comm (A):
-      ∀a. a ⨮ Ⓔ = Ⓔ ⨭{A} a.
+      ∀a. a ⨮ ⓔ = ⓔ ⨭{A} a.
 // qed.
 
 lemma list_cons_shift (A):