update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
index 2dcf8e5767bf41807995257ae8b831b4a547f579..13c68a33cb38843ec0f184012af2d3a4a803eac8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
@@ -29,7 +29,7 @@ interpretation
 (* Basic constructions ******************************************************)
 
 lemma list_append_empty_sn (A):
-      â\88\80l2. l2 = â\92º ⨁{A} l2.
+      â\88\80l2. l2 = â\93\94 ⨁{A} l2.
 // qed.
 
 lemma list_append_lcons_sn (A):
@@ -39,7 +39,7 @@ lemma list_append_lcons_sn (A):
 (* Advanced constructions ***************************************************)
 
 lemma list_append_empty_dx (A):
-      â\88\80l1. l1 = l1 â¨\81{A} â\92º.
+      â\88\80l1. l1 = l1 â¨\81{A} â\93\94.
 #A #l1 elim l1 -l1
 [ <list_append_empty_sn //
 | #hd #tl #IH <list_append_lcons_sn <IH //