From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Thu, 13 Oct 2011 15:25:40 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~2194
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ae7b573a31d8843d03977c5eeb3ec14576fb4985;p=helm.git

commit by user andrea
---

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index ad0896d70..d564b7220 100644
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -77,6 +77,19 @@ For Matita, the task is trivial and we can simply close the goal with // *)
 
 // qed.
 
+(* COERCIONS *)
+
+inductive bool : Type[0] ≝
+| tt : bool
+| ff : bool.
+
+definition nat_of_bool ≝ λb. match b with 
+[ tt ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a 
+| ff ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a 
+].
+
+(* coercion nat_of_bool. ?? *)
+ 
 (* Let us now define the following function: *)
 
 definition twice ≝ λn.a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a n n. 
@@ -138,29 +151,30 @@ qed.
 
 (* Instead of proving the existence of a number corresponding to the half of n, we could
 be interested in computing it. The best way to do it is to define this division operation
-together with the remainder, that is 0 if the input term is even, and 1 if the input term
-is odd. Since we must return a pair, we could use a suitably defined record type, or simply
-a product type N × N, defined in the basic library. The product type is just a sort of
-general purpose record, with standard fields fst and snd, called projections. A pair of
-values n and m is written (pair … m n) or \langle n,m \rangle - visually rendered as 〈n,m〉 
+together with the remainder, that in our case is just a boolean value: tt if the input term 
+is even, and ff if the input term is odd. Since we must return a pair, we could use a 
+suitably defined record type, or simply a product type nat × bool, defined in the basic library. 
+The product type is just a sort of general purpose record, with standard fields fst and snd, 
+called projections. A pair of values n and m is written (pair … m n) or \langle n,m \rangle - 
+visually rendered as 〈n,m〉 
 
 We first write down the function, and then discuss it.*)
 
 let rec div2 n ≝ 
 match n with
-[ O ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a,a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉
+[ O ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉
 | S a ⇒ span style="text-decoration: underline;"/span
    let p ≝ (div2 a) in
    match (a href="cic:/matita/basics/types/snd.def(1)"snd/a … p) with
-   [ O ⇒ 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/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉
-   | S b ⇒ 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/nat.con(0,1,0)"O/a〉 
+   [ tt ⇒ 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〉 
+   | ff ⇒ 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〉
    ]
 ]. 
 
-(* The function is computed by recursion over the input n. If n is 0, then both quotient
-and remainder are 0. If n = S a, we start computing the half of a, say 〈q,r〉. Then we
-have two cases according to the possible values of b: if b is 0, then we must return
- 〈q,1〉, while if b = 1 (no other case is possible), then we must return 〈S q,0〉.
+(* The function is computed by recursion over the input n. If n is 0, then the quotient
+is 0 and the remainder is tt. If n = S a, we start computing the half of a, say 〈q,b〉. 
+Then we have two cases according to the possible values of b: if b is tt, then we must return
+ 〈q,ff〉, while if b = ff then we must return 〈S q,tt〉.
 
 It is important to point out the deep, substantial analogy between the algorithm for 
 computing div2 and the the proof of ex_half. In particular ex_half returns a 
@@ -169,7 +183,7 @@ n and a boolean indicating which one between the two conditions A(n) and B(n) is
 This is precisely the quotient-remainder pair returned by div2.
 In both cases we proceed by recurrence (respectively, induction or recursion) over the 
 input argument n. In case n = 0, we conclude the proof in ex_half by providing the
-witness O and a proof of A(O); this corresponds to returning the pair 〈O,O〉 in div2.
+witness O and a proof of A(O); this corresponds to returning the pair 〈O,tt〉 in div2.
 Similarly, in the inductive case n = S a, we must exploit the inductive hypothesis 
 for a (i.e. the result of the recursive call), distinguishing two subcases according 
 to the the two possibilites A(a) or B(a) (i.e. the two possibile values of the remainder 
@@ -181,22 +195,21 @@ Let us now prove that our div2 function has the expected behaviour.
 lemma surjective_pairing: ∀A,B.∀p:Aa title="Product" href="cic:/fakeuri.def(1)"×/aB. 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 title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a … p〉.
 #A #B * // qed.
 
-lemma div2SO: ∀n,q. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉 → a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aspan style="text-decoration: underline;"/spanq, a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉.
+lemma div2SO: ∀n,q. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉 → a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aspan style="text-decoration: underline;"/spanq,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉.
 #n #q #H normalize >H normalize // qed.
 
-lemma div2S1: ∀n,q. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉 → a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a q,a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉.
+lemma div2S1: ∀n,q. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉 → a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a q,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉.
 #n #q #H normalize >H normalize // qed.
 
- lemma div2_ok: ∀n,q,r. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,r〉 →
-   r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a span style="text-decoration: underline;"/spana title="logical and" href="cic:/fakeuri.def(1)"∧/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q a title="logical or" href="cic:/fakeuri.def(1)"∨/a 
-   r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q).
+lemma div2_ok: ∀n,q,r. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,r〉 → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q) (a href="cic:/matita/tutorial/chapter2/nat_of_bool.def(1)"nat_of_bool/a r).
 #n elim n
-  [#q #r normalize #H destruct %1 /2/
-  |#a #Hind #q #r cases (Hind … (a href="cic:/matita/tutorial/chapter2/surjective_pairing.def(3)"surjective_pairing/a …)) * #eqr #eqa
-    [>(a href="cic:/matita/tutorial/chapter2/div2SO.def(3)"div2SO/a a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a))) // #H %2 destruct <eqa /2/
-    |>(a href="cic:/matita/tutorial/chapter2/div2S1.def(3)"div2S1/a a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a))) // #H %1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a <eqa /2/
+  [#q #r normalize #H destruct //
+  |#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/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.
 
 (* There is still another possibility, however, namely to mix the program and its 
@@ -219,27 +232,31 @@ record Sub (A:Type[0]) (P:A → Prop) : Type[0] ≝
   {witness: A; 
    proof: P witness}.
 
- definition div2Spec ≝ λn.λp.∀q,r. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,r〉 →
-  r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a span style="text-decoration: underline;"/spana title="logical and" href="cic:/fakeuri.def(1)"∧/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q a title="logical or" href="cic:/fakeuri.def(1)"∨/a 
-  r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q).
-
-(* We can now construct a function from n to {p|div2Spec n p} by composing the objects
+definition qr_spec ≝ λn.λp.∀q,r. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,r〉 → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q) (a href="cic:/matita/tutorial/chapter2/nat_of_bool.def(1)"nat_of_bool/a r).
+  
+(* We can now construct a function from n to {p|qr_spec n p} by composing the objects
 we already have *)
 
-definition div2P: ∀n.a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)" Sub/a (a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/aa title="Product" href="cic:/fakeuri.def(1)"×/aa href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/a) (a href="cic:/matita/tutorial/chapter2/div2Spec.def(3)"div2Spec/a n) ≝ λn.
+definition div2P: ∀n.a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)" Sub/a (a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/aa title="Product" href="cic:/fakeuri.def(1)"×/aspan style="text-decoration: underline;"a href="cic:/matita/tutorial/chapter2/bool.ind(1,0,0)"bool/a/span) (a href="cic:/matita/tutorial/chapter2/qr_spec.def(3)"qr_spec/a n) ≝ λn.
  a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a ?? (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n) (a href="cic:/matita/tutorial/chapter2/div2_ok.def(4)"div2_ok/a n).
 
 (* But we can also try do directly build such an object *)
 
-definition div2Pbis : ∀n.a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)"Sub/a (a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/aa title="Product" href="cic:/fakeuri.def(1)"×/aa href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/a) (a href="cic:/matita/tutorial/chapter2/div2Spec.def(3)"div2Spec/a n).
+definition div2Pagain : ∀n.a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)"Sub/a (a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/aa title="Product" href="cic:/fakeuri.def(1)"×/aspan style="text-decoration: underline;"/spana href="cic:/matita/tutorial/chapter2/bool.ind(1,0,0)"bool/a) (a href="cic:/matita/tutorial/chapter2/qr_spec.def(3)"qr_spec/a n).
 #n elim n
-  [@(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,1,0)"O/a,a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉) normalize #q #r #H %1 destruct /2/
-  |#a * #p #spec cases (spec … (a href="cic:/matita/tutorial/chapter2/surjective_pairing.def(3)"surjective_pairing/a …)) * #eqr #eqa
-    [@(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/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉) #q #r #H %2 destruct /2/ 
-    |@(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/nat.con(0,1,0)"O/a〉) #q #r #H %1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a /2/
-    ]
+  [@(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,1,0)"O/a,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉) normalize #q #r #H destruct //
+  |#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/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.
 
+example quotient7: a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"witness/a … (a href="cic:/matita/tutorial/chapter2/div2P.def(5)"div2P/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/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/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a)),a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉.
+// qed.
 
-lemma foo: True. 
-pre /pre
\ No newline at end of file
+example quotient8: a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"witness/a … (a href="cic:/matita/tutorial/chapter2/div2P.def(5)"div2P/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/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/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a))), a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉.
+// qed. 
+prepre /pre/pre
\ No newline at end of file