+\ 5img class="anchor" src="icons/tick.png" id="exhint"\ 6example exhint: ∀b:\ 5a href="cic:/matita/tutorial/chapter4/DeqBool.def(5)"\ 6DeqBool\ 5/a\ 6. (b\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+#b #H @(\P H)
+qed.
+
+(* The point is that == expects in input a pair of objects whose type must be the
+carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the type inference
+system has no knowledge of it (it is an information that has been supplied by the
+user, and stored somewhere in the library). More explicitly, the type inference
+inference system, would face an unification problem consisting to unify bool
+against the carrier of something (a metavaribale) and it has no way to synthetize
+the answer. To solve this kind of situations, matita provides a mechanism to hint
+the system the expected solution. A unification hint is a kind of rule, whose rhd
+is the unification problem, containing some metavariables X1, ..., Xn, and whose
+left hand side is the solution suggested to the system, in the form of equations
+Xi=Mi. The hint is accepted by the system if and only the solution is correct, that
+is, if it is a unifier for the given problem.
+To make an example, in the previous case, the unification problem is bool = carr X,
+and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since
+bool is convertible with (carr (mk_DeqSet bool beb true)). *)
+
+unification hint 0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 ;
+ X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6