-definition DeqProd ≝ λA,B:DeqSet.
- mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
-
-unification hint 0 ≔ C1,C2;
- T1 ≟ carr C1,
- T2 ≟ carr C2,
- X ≟ DeqProd C1 C2
+\ 5img class="anchor" src="icons/tick.png" id="DeqProd"\ 6definition DeqProd ≝ λA,B:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.
+ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 (A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B) (\ 5a href="cic:/matita/tutorial/chapter4/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 A B) (\ 5a href="cic:/matita/tutorial/chapter4/eq_pairs_true.def(6)"\ 6eq_pairs_true\ 5/a\ 6 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 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 C1,C2;
+ T1 ≟ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 C1,
+ T2 ≟ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 C2,
+ X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqProd.def(7)"\ 6DeqProd\ 5/a\ 6 C1 C2