+
+\ 5pre class="smallmargin" style="display: inline;"\ 6\ 5img class="anchor" src="icons/tick.png" id="eq_map"\ 6lemma eq_map : ∀A,B,f,g,l. (∀x.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
+#A #B #f #g #l #eqfg (elim l) normalize // qed. \ 5/pre\ 6
+
+(**************************** fold right ******************************)
+\ 5img class="anchor" src="icons/tick.png" id="foldr"\ 6let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝