X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter2.ma;h=ab758c124f52fafb842e8e3bd4246b61346c2aa6;hb=f848433620419e71cd19ec0b4f58c717ac50f85e;hp=804ba58ba3c74d6771881c10e131f5bfa8478868;hpb=01d39f9b4feb6eba25f951c6fda8037840db88b4;p=helm.git

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 804ba58ba..ab758c124 100644
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -217,7 +217,7 @@ lemma div2_ok: ∀n,q,r. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
   |#a #Hind #q #r 
    cut (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a), a href="cic:/matita/basics/types/snd.def(1)"snd/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a)〉) [//] 
    cases (a href="cic:/matita/basics/types/snd.def(1)"snd/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a))
-    [#H >(a href="cic:/matita/tutorial/chapter2/div2S1.def(3)"div2S1/a … H) #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a <a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @(Hind … H) 
+    [#H >(a href="cic:/matita/tutorial/chapter2/div2S1.def(3)"div2S1/a … H) #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a whd in ⊢ (???%); <a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @(Hind … H) 
     |#H >(a href="cic:/matita/tutorial/chapter2/div2SO.def(3)"div2SO/a … H) #H1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a @(Hind … H) 
     ]
 qed.
@@ -259,7 +259,8 @@ definition div2Pagain : ∀n.a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,
   |#a * #p #qrspec 
    cut (p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p, a href="cic:/matita/basics/types/snd.def(1)"snd/a … p〉) [//] 
    cases (a href="cic:/matita/basics/types/snd.def(1)"snd/a … p)
-    [#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉) whd #q #r #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a <a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @(qrspec … H)
+    [#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉) whd #q #r #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a
+     whd in ⊢ (???%); <a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @(qrspec … H)
     |#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉) whd #q #r #H1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a @(qrspec … H) 
   ]
 qed.