+definition map_again ≝ λA,B,f,l. \ 5a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 A (\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) (λa,l.f a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] l.
+
+(* Can we prove that map_again is "the same" as map? We should first of all
+clarify in which sense we expect the two functions to be equal. Equality in
+Matita has an intentional meaning: it is the smallest predicate induced by
+convertibility, i.e. syntactical equality up to normalization. From an
+intentional point of view, map and map_again are not functions, but programs,
+and they are clearly different. What we would like to say is that the two
+programs behave in the same way: this is a different, extensional equality
+that can be defined in the following way. *)
+
+definition ExtEq ≝ λA,B:Type[0].λf,g:A→B.∀a:A.f a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g a.
+
+(* Proving that map and map_again are extentionally equal in the
+previous sense can be proved by a trivial structural induction on the list *)
+
+lemma eq_maps: ∀A,B,f. \ 5a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"\ 6ExtEq\ 5/a\ 6 ?? (\ 5a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f) (\ 5a href="cic:/matita/tutorial/chapter3/map_again.def(2)"\ 6map_again\ 5/a\ 6 A B f).
+#A #B #f #n (elim n) normalize // qed.
+
+(* Let us make another remark about extensional equality. It is clear that,
+if f is extensionally equal to g, then (map A B f) is extensionally equal to
+(map A B g). Let us prove it. *)
+
+theorem eq_map : ∀A,B,f,g. \ 5a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"\ 6ExtEq\ 5/a\ 6 A B f g → \ 5a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"\ 6ExtEq\ 5/a\ 6 ?? (\ 5a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"\ 6map\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6A B f) (\ 5a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g).
+#A #B #f #g #eqfg
+
+(* the relevant point is that we cannot proceed by rewriting f with g via
+eqfg, here. Rewriting only works with Matita intensional equality, while here
+we are dealing with a different predicate, defined by the user. The right way
+to proceed is to unfold the definition of ExtEq, and work by induction on l,
+as usual when we want to prove extensional equality between functions over
+inductive types; again the rest of the proof is trivial. *)
+
+#l (elim l) normalize // qed.
+
+(**************************** BIGOPS *******************************)
+
+(* Building a library of basic functions, it is important to achieve a
+good degree of abstraction and generality, in order to be able to reuse
+suitable instances of the same function in different context. This has not
+only the obvious benefit of factorizing code, but especially to avoid
+repeating proofs of generic properties over and over again.
+A really convenient tool is the following combination of fold and filter,
+that essentially allow you to iterate on every subset of a given enumerated
+(finite) type, represented as a list. *)
+
+ let rec fold (A,B:Type[0]) (op:B→B→B) (b:B) (p:A→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"\ 6bool\ 5/a\ 6) (f:A→B) (l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l:B ≝