(* *)
(**************************************************************************)
+include "hints_declaration.ma".
include "logic/equality.ma".
include "sets/setoids.ma".
napply mk_setoid [ napply nat | napply EQ]
nqed.
-unification hint 0 ((λx,y.True) (carr NAT) nat).
\ No newline at end of file
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 0 ≔ ⊢ carr NAT ≡ nat.