update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma
index 66ce703a81fc118fbd36ee1d255c87771e38fb9c..a0ba8d77b922ffa4be96f7b5292ee8fbc536ece3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma
@@ -37,13 +37,13 @@ lemma list_length_lcons (A:Type[0]) (l:list A) (a:A): |a⨮l| = ↑|l|.
 (* Basic inversions *********************************************************)
 
 lemma list_length_inv_zero_dx (A:Type[0]) (l:list A):
-      |l| = ð\9d\9f\8e â\86\92 l = â\92º.
+      |l| = ð\9d\9f\8e â\86\92 l = â\93\94.
 #A * // #a #l >list_length_lcons #H
 elim (eq_inv_nsucc_zero … H)
 qed-.
 
 lemma list_length_inv_zero_sn (A:Type[0]) (l:list A):
-      (ð\9d\9f\8e) = |l| â\86\92 l = â\92º.
+      (ð\9d\9f\8e) = |l| â\86\92 l = â\93\94.
 /2 width=1 by list_length_inv_zero_dx/ qed-.
 
 lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x):