commit by user andrea

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 2c98ad147c621a560b3ad8c47ad00fface2a0ab4..c159fa13db6b0dfe72246273c57a1db5ecab7236 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -278,7 +278,10 @@ example exhint1: ∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6
 #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,