X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter4.ma;h=c159fa13db6b0dfe72246273c57a1db5ecab7236;hb=bef004f9c2ab68f9f0f9c95536918681a61849fc;hp=2c98ad147c621a560b3ad8c47ad00fface2a0ab4;hpb=b12c549230b2232b31e443942c20be615455b0ad;p=helm.git

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 2c98ad147..c159fa13d 100644
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -278,7 +278,10 @@ example exhint1: ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a
 #b #H @(\P H)
 qed.
 
-(* pairs *)
+(* The cartesian product of two DeqSets is still a DeqSet. To prove
+this, we must as usual define the boolen equality function, and prove
+it correctly reflects propositional equality. *)
+
 definition eq_pairs ≝
   λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
 
@@ -292,7 +295,12 @@ qed.
 
 definition DeqProd ≝ λA,B:DeqSet.
   mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
-  
+
+(* Having an unification problem of the kind T1×T2 = carr X, what kind 
+of hint can we give to the system? We expect T1 to be the carrier of a
+DeqSet C1, T2 to be the carrier of a DeqSet C2, and X to be DeqProd C1 C2.
+This is expressed by the following hint: *)
+
 unification hint  0 ≔ C1,C2; 
     T1 ≟ carr C1,
     T2 ≟ carr C2,