commit by user andrea

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index cafb853238a123e37b8500f17cbb727b15d0dc58..f822ce6f7d506cbb9a9a7f1f67673c2d377ab33e 100644 (file)
--- a/weblib/tutorial/chapter3.ma
+++ b/weblib/tutorial/chapter3.ma
@@ -83,10 +83,8 @@ 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.
 #A #B #f #g #l #eqfg (elim l) normalize // qed.
-*)
 
 (*
 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝