From: matitaweb Date: Fri, 14 Oct 2011 11:20:38 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2184 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3e2852f2bff956dddaa3f1d2350ba75987cc9e75;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma index f822ce6f7..d7b6d4f1e 100644 --- a/weblib/tutorial/chapter3.ma +++ b/weblib/tutorial/chapter3.ma @@ -83,7 +83,7 @@ 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. +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/tutorial/chapter3/map.fix(0,3,1)"map/a span style="text-decoration: underline;"/spanA B f l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"map/a A B g l. #A #B #f #g #l #eqfg (elim l) normalize // qed. (*