+
+unification hint 1 ≔
+ A:setoid, B,C : 𝛀^A;
+ R ≟ (mk_binary_morphism1 (ext_powerclass_setoid A) (ext_powerclass_setoid A) (ext_powerclass_setoid A)
+ (λS,S':carr1 (ext_powerclass_setoid A).
+ mk_ext_powerclass A (S∩S') (ext_prop A (intersect_is_ext ? S S')))
+ (prop21 … (intersect_is_ext_morph A))) ,
+ BB ≟ (ext_carr ? B),
+ CC ≟ (ext_carr ? C)
+ (* ------------------------------------------------------*) ⊢
+ ext_carr A
+ (fun21
+ (ext_powerclass_setoid A)
+ (ext_powerclass_setoid A)
+ (ext_powerclass_setoid A) R B C) ≡
+ intersect (carr A) BB CC.
+
+(*
+alias symbol "hint_decl" = "hint_decl_Type2".
+unification hint 0 ≔
+ A : setoid, B,C : 𝛀^A ;
+ CC ≟ (ext_carr ? C),
+ BB ≟ (ext_carr ? B),
+ C1 ≟ (carr1 (powerclass_setoid (carr A))),
+ C2 ≟ (carr1 (ext_powerclass_setoid A))
+ ⊢
+ eq_rel1 C1 (eq1 (powerclass_setoid (carr A))) BB CC ≡
+ eq_rel1 C2 (eq1 (ext_powerclass_setoid A)) B C.
+
+unification hint 0 ≔
+ A, B : CPROP ⊢ iff A B ≡ eq_rel1 ? (eq1 CPROP) A B.