+
+unification hint 1 ≔
+ AA : setoid, B,C : 𝛀^AA;
+ A ≟ carr AA,
+ T ≟ ext_powerclass_setoid AA,
+ R ≟ mk_unary_morphism1 ?? (λX:𝛀^AA.
+ mk_unary_morphism1 ?? (λY:𝛀^AA.
+ mk_ext_powerclass AA
+ (ext_carr ? X - ext_carr ? Y)
+ (ext_prop AA (substract_is_ext ? X Y)))
+ (prop11 ?? (fun11 ?? (substract_is_ext_morph AA) X)))
+ (prop11 ?? (substract_is_ext_morph AA)),
+ BB ≟ (ext_carr ? B),
+ CC ≟ (ext_carr ? C)
+(*------------------------------------------------------*) ⊢
+ ext_carr AA (fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C) ≡ substract A BB CC.
+
+(* hints for {x} *)
+nlemma single_is_morph : ∀A:setoid. (setoid1_of_setoid A) ⇒_1 Ω^A.
+#X; @; ##[ napply (λx.{(x)}); ##]
+#a b E; napply ext_set; #x; @; #H; /3/; nqed.
+
+nlemma single_is_ext: ∀A:setoid. A → 𝛀^A.
+#X a; @; ##[ napply ({(a)}); ##] #x y E; @; #H; /3/; nqed.
+
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 0 ≔ A : setoid, a : carr A;
+ R ≟ (mk_ext_powerclass ? {(a)} (ext_prop ? (single_is_ext ? a)))
+(*-------------------------------------------------------------------------*) ⊢
+ ext_carr A R ≡ singleton A a.
+
+unification hint 0 ≔ A:setoid, a : carr A;
+ T ≟ setoid1_of_setoid A,
+ AA ≟ carr A,
+ MM ≟ mk_unary_morphism1 ??
+ (λa:carr1 (setoid1_of_setoid A).{(a)}) (prop11 ?? (single_is_morph A))
+(*--------------------------------------------------------------------------*) ⊢
+ fun11 T (powerclass_setoid AA) MM a ≡ {(a)}.
+
+nlemma single_is_ext_morph:∀A:setoid.(setoid1_of_setoid A) ⇒_1 𝛀^A.
+#A; @; ##[ #a; napply (single_is_ext ? a); ##] #a b E; @; #x; /3/; nqed.
+
+unification hint 1 ≔ AA : setoid, a: carr AA;
+ T ≟ ext_powerclass_setoid AA,
+ R ≟ mk_unary_morphism1 ??
+ (λa:carr1 (setoid1_of_setoid AA).
+ mk_ext_powerclass AA {(a)} (ext_prop ? (single_is_ext AA a)))
+ (prop11 ?? (single_is_ext_morph AA))
+(*------------------------------------------------------*) ⊢
+ ext_carr AA (fun11 (setoid1_of_setoid AA) T R a) ≡ singleton AA a.
+
+
+(*
+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.