commit by user andrea

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index f822ce6f7d506cbb9a9a7f1f67673c2d377ab33e..d7b6d4f1e5471b3e009d74e0a5191b5debb94c5a 100644 (file)
--- a/weblib/tutorial/chapter3.ma
+++ b/weblib/tutorial/chapter3.ma
@@ -83,7 +83,7 @@ lemma filter_false : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/f
   \ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"\ 6filter\ 5/a\ 6 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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/basics/list/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/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
+theorem 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/tutorial/chapter3/map.fix(0,3,1)"\ 6map\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 
 (*