From: matitaweb Date: Fri, 14 Oct 2011 10:45:24 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2185 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1309af9ce5241646b925a37206c2798cf846dced;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma index cafb85323..f822ce6f7 100644 --- a/weblib/tutorial/chapter3.ma +++ b/weblib/tutorial/chapter3.ma @@ -83,10 +83,8 @@ lemma filter_false : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/f a href="cic:/matita/tutorial/chapter3/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/tutorial/chapter3/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. #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 ≝