X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter7.ma;h=55a830179bdacb4e54c98f24e8a14ec67101554c;hb=ceb81586cd493164f9c980c4f97ed0b4dbc6f545;hp=17316f03169fc9a3707999b29b69298d9612ab8a;hpb=a2ba04cd90e76937720b16e37cb12a39b46181e3;p=helm.git

diff --git a/weblib/tutorial/chapter7.ma b/weblib/tutorial/chapter7.ma
index 17316f031..55a830179 100644
--- a/weblib/tutorial/chapter7.ma
+++ b/weblib/tutorial/chapter7.ma
@@ -229,11 +229,11 @@ interpretation "in_prl" 'in_l E = (in_prl ? E).
 (* The following, trivial lemmas are only meant for rewriting purposes. *)
 
 lemma sem_pre_true : ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. 
-  a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉} a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a}. 
+  a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉} a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a}. 
 // qed.
 
 lemma sem_pre_false : ∀S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. 
-  a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉} a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i}. 
+  a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a〉} a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{i}. 
 // qed.
 
 lemma sem_cat: ∀S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.