X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Flist_length.ma;h=e4df2ae4df2637746456ae41874fec02c9d0740a;hb=cc178d85bc4fec05b6a9dd176f338b3275beb3d9;hp=a0ba8d77b922ffa4be96f7b5292ee8fbc536ece3;hpb=5489d0b66ed7bff17b9dedb89708f57f1d542adc;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma
index a0ba8d77b..e4df2ae4d 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground/notation/functions/verticalbars_1.ma". 
 include "ground/lib/list.ma".
 include "ground/arith/nat_succ.ma".
 
@@ -24,31 +25,33 @@ rec definition list_length A (l:list A) on l ≝ match l with
 
 interpretation
   "length (lists)"
-  'card l = (list_length ? l).
+  'VerticalBars l = (list_length ? l).
 
 (* Basic constructions ******************************************************)
 
-lemma list_length_empty (A:Type[0]): |list_empty A| = 𝟎.
+lemma list_length_empty (A:Type[0]):
+      ❘list_empty A❘ = 𝟎.
 // qed.
 
-lemma list_length_lcons (A:Type[0]) (l:list A) (a:A): |a⨮l| = ↑|l|.
+lemma list_length_lcons (A:Type[0]) (l:list A) (a:A):
+      ❘a⨮l❘ = ↑❘l❘.
 // qed.
 
 (* Basic inversions *********************************************************)
 
 lemma list_length_inv_zero_dx (A:Type[0]) (l:list A):
-      |l| = 𝟎 → l = ⓔ.
+      ❘l❘ = 𝟎 → l = ⓔ.
 #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):
-      (𝟎) = |l| → l = ⓔ.
+      (𝟎) = ❘l❘ → l = ⓔ.
 /2 width=1 by list_length_inv_zero_dx/ qed-.
 
 lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x):
-      |l| = ↑x →
-      ∃∃tl,a. x = |tl| & l = a ⨮ tl.
+      ❘l❘ = ↑x →
+      ∃∃tl,a. x = ❘tl❘ & l = a ⨮ tl.
 #A *
 [ #x >list_length_empty #H
   elim (eq_inv_zero_nsucc … H)
@@ -58,6 +61,6 @@ lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x):
 qed-.
 
 lemma list_length_inv_succ_sn (A:Type[0]) (l:list A) (x):
-      ↑x = |l| →
-      ∃∃tl,a. x = |tl| & l = a ⨮ tl.
+      ↑x = ❘l❘ →
+      ∃∃tl,a. x = ❘tl❘ & l = a ⨮ tl.
 /2 width=1 by list_length_inv_succ_dx/ qed-.