X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flist.ma;h=49cc0a5afc548a567fe03d138d4c2649ab5b0aae;hb=41b61472d2c475e0f69e3dfc85539da3ad2bac1e;hp=245a9fd3b4789818833887095b8db4cb1e04a1cf;hpb=a5c551d0b7399f00e8eef3dfb06e2a0895eac3d4;p=helm.git

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index 245a9fd3b..49cc0a5af 100644
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -19,7 +19,7 @@ notation "hvbox(hd break :: tl)"
   right associative with precedence 47
   for @{'cons $hd $tl}.
 
-notation "[ list0 x sep ; ]"
+notation "ref 'cons [ list0 x sep ; ref 'nil ]"
   non associative with precedence 90
   for ${fold right @'nil rec acc @{'cons $x $acc}}.
 
@@ -34,8 +34,8 @@ definition not_nil: ∀A:Type[0].a href="cic:/matita/basics/list/list.ind(1,0,1
  λA.λl.match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons hd tl ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a ].
 
 theorem nil_cons:
-  ∀A:Type[0].∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a:A. aa title="cons" href="cic:/fakeuri.def(1)":/a:l a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a title="nil" href="cic:/fakeuri.def(1)"[/a].
-  #A #l #a @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq (change with (a href="cic:/matita/basics/list/not_nil.def(1)"not_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/a:l))) >Heq //
+  ∀A:Type[0].∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a:A. aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a.
+  #A #l #a @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq (change with (a href="cic:/matita/basics/list/not_nil.def(1)"not_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al))) >Heq //
 qed.
 
 (*
@@ -47,17 +47,17 @@ let rec id_list A (l: list A) on l :=
 let rec append A (l1: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) l2 on l1 ≝ 
   match l1 with
   [ nil ⇒  l2
-  | cons hd tl ⇒  hd a title="cons" href="cic:/fakeuri.def(1)":/a: append A tl l2 ].
+  | cons hd tl ⇒  hd a title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/a append A tl l2 ].
 
 definition hd ≝ λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.λd:A.
   match l with [ nil ⇒ d | cons a _ ⇒ a].
 
 definition tail ≝  λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
-  match l with [ nil ⇒  a title="nil" href="cic:/fakeuri.def(1)"[/a] | cons hd tl ⇒  tl].
+  match l with [ nil ⇒  a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a | cons hd tl ⇒  tl].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
-theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
+theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
 #A #l (elim l) normalize // qed.
 
 theorem associative_append: 
@@ -70,24 +70,24 @@ ntheorem cons_append_commute:
     a :: (l1 @ l2) = (a :: l1) @ l2.
 //; nqed. *)
 
-theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:l1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]))a title="append" href="cic:/fakeuri.def(1)"@/al1.span style="text-decoration: underline;"/spanspan class="autotactic"/span
+theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a))a title="append" href="cic:/fakeuri.def(1)"@/al1.span style="text-decoration: underline;"/spanspan class="autotactic"/span
 #A #a #l1 #l2 >a href="cic:/matita/basics/list/associative_append.def(4)"associative_append/a // qed.
 
 theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀P:?→?→Prop. 
-  l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="nil" href="cic:/fakeuri.def(1)"[/a] → P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) → P l1 l2.
+  l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a → P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) → P l1 l2.
 #A #l1 #l2 #P (cases l1) normalize //
 #a #l3 #heq destruct
 qed.
 
 theorem nil_to_nil:  ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
-  l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a].
+  l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a.
 #A #l1 #l2 #isnil @(a href="cic:/matita/basics/list/nil_append_elim.def(4)"nil_append_elim/a A l1 l2) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
 qed.
 
 (* iterators *)
 
 let rec map (A,B:Type[0]) (f: A → B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B ≝
- match l with [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ? | cons x tl ⇒ f x a title="cons" href="cic:/fakeuri.def(1)":/a: (map A B f tl)].
+ match l with [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ? | cons x tl ⇒ f x a title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/a (map A B f tl)].
   
 lemma map_append : ∀A,B,f,l1,l2.
   (a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l1) a title="append" href="cic:/fakeuri.def(1)"@/a (a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f (l1a title="append" href="cic:/fakeuri.def(1)"@/al2).
@@ -101,17 +101,17 @@ let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:a href="cic:/matita/basi
  
 definition filter ≝ 
   λT.λp:T → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.
-  a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T) (λx,l0.if (p x) then (xa title="cons" href="cic:/fakeuri.def(1)":/a:l0) else l0) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a T).
+  a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T) (λx,l0.if (p x) then (xa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al0) else l0) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a T).
 
 definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
-    a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a ?? (λi,acc.(a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (f i) l2)a title="append" href="cic:/fakeuri.def(1)"@/aacc) a title="nil" href="cic:/fakeuri.def(1)"[/a ] l1.
+    a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a ?? (λi,acc.(a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (f i) l2)a title="append" href="cic:/fakeuri.def(1)"@/aacc) a title="nil" href="cic:/fakeuri.def(1)"[/a a title="nil" href="cic:/fakeuri.def(1)"]/a l1. 
 
 lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
-  a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="cons" href="cic:/fakeuri.def(1)":/a: a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l.
+  a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/a a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
 lemma filter_false : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → 
-  a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l.
+  a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
 theorem eq_map : ∀A,B,f,g,l. (∀x.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g x) → a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B g l.
@@ -124,6 +124,46 @@ match l1 with
   | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
   ]. *)
 
+(**************************** reverse *****************************)
+let rec rev_append S (l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S) on l1 ≝
+  match l1 with 
+  [ nil ⇒ l2
+  | cons a tl ⇒ rev_append S tl (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al2)
+  ]
+.
+
+definition reverse ≝λS.λl.a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"rev_append/a S l a title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a.
+
+lemma reverse_single : ∀S,a. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a). 
+// qed.
+
+lemma rev_append_def : ∀S,l1,l2. 
+  a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"rev_append/a S l1 l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l1) a title="append" href="cic:/fakeuri.def(1)"@/a l2 .
+#S #l1 elim l1 normalize // 
+qed.
+
+lemma reverse_cons : ∀S,a,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l)a title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a).
+#S #a #l whd in ⊢ (??%?); // 
+qed.
+
+lemma reverse_append: ∀S,l1,l2. 
+  a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (l1 a title="append" href="cic:/fakeuri.def(1)"@/a l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l2)a title="append" href="cic:/fakeuri.def(1)"@/a(a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a
+>a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a // qed.
+
+lemma reverse_reverse : ∀S,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
+#S #l elim l // #a #tl #Hind >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a >a href="cic:/matita/basics/list/reverse_append.def(8)"reverse_append/a 
+normalize // qed.
+
+(* an elimination principle for lists working on the tail;
+useful for strings *)
+lemma list_elim_left: ∀S.∀P:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S → Prop. P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a S) →
+(∀a.∀tl.P tl → P (tla title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a))) → ∀l. P l.
+#S #P #Pnil #Pstep #l <(a href="cic:/matita/basics/list/reverse_reverse.def(9)"reverse_reverse/a … l) 
+generalize in match (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l); #l elim l //
+#a #tl #H >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a @Pstep //
+qed.
+
 (**************************** length *******************************)
 
 let rec length (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝ 
@@ -135,7 +175,7 @@ notation "|M|" non associative with precedence 60 for @{'norm $M}.
 interpretation "norm" 'norm l = (length ? l).
 
 lemma length_append: ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. 
-  a title="norm" href="cic:/fakeuri.def(1)"|/al1a title="append" href="cic:/fakeuri.def(1)"@/al2| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/al1|a title="natural plus" href="cic:/fakeuri.def(1)"+/aa title="norm" href="cic:/fakeuri.def(1)"|/al2|.
+  a title="norm" href="cic:/fakeuri.def(1)"|/al1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="norm" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/al1a title="norm" href="cic:/fakeuri.def(1)"|/aa title="natural plus" href="cic:/fakeuri.def(1)"+/aa title="norm" href="cic:/fakeuri.def(1)"|/al2a title="norm" href="cic:/fakeuri.def(1)"|/a.
 #A #l1 elim l1 // normalize /span class="autotactic"2span class="autotrace" trace /span/span/
 qed.
 
@@ -165,20 +205,20 @@ interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
 
 theorem fold_true: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
-  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-    op (f a) a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i). 
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+    op (f a) a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i). 
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
 theorem fold_false: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
-p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i).
+p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i).
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
 theorem fold_filter: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
-  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
-    a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ (a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l)} (f i).
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+    a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ (a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l)a title="\fold" href="cic:/fakeuri.def(1)"}/a (f i).
 #A #B #a #l #p #op #nil #f elim l //  
 #a #tl #Hind cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p a)) #pa 
   [ >a href="cic:/matita/basics/list/filter_true.def(3)"filter_true/a // > a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a // >a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a //
@@ -193,8 +233,8 @@ record Aop (A:Type[0]) (nil:A) : Type[0] ≝
   }.
 
 theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀nil.∀op:a href="cic:/matita/basics/list/Aop.ind(1,0,2)"Aop/a B nil.∀f.
-  op (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈I} (f i)) (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈J} (f i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
-    a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈(Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)} (f i).
+  op (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈Ia title="\fold" href="cic:/fakeuri.def(1)"}/a (f i)) (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈Ja title="\fold" href="cic:/fakeuri.def(1)"}/a (f i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+    a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈(Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)a title="\fold" href="cic:/fakeuri.def(1)"}/a (f i).
 #A #B #I #J #nil #op #f (elim I) normalize 
   [>a href="cic:/matita/basics/list/nill.fix(0,2,2)"nill/a //|#a #tl #Hind <a href="cic:/matita/basics/list/assoc.fix(0,2,2)"assoc/a //]
 qed.
\ No newline at end of file