+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 0 ≔
+ A : setoid, B,C : 𝛀^A;
+ R ≟ (mk_ext_powerclass ? (B ∪ C) (ext_prop ? (union_is_ext ? B C)))
+(*-------------------------------------------------------------------------*) ⊢
+ ext_carr A R ≡ union ? (ext_carr ? B) (ext_carr ? C).
+
+unification hint 0 ≔ S:Type[0], A,B:Ω^S;
+ MM ≟ mk_unary_morphism1 ??
+ (λA.mk_unary_morphism1 ?? (λB.A ∪ B) (prop11 ?? (union_is_morph S A)))
+ (prop11 ?? (union_is_morph S))
+(*--------------------------------------------------------------------------*) ⊢
+ fun11 ?? (fun11 ?? MM A) B ≡ A ∪ B.
+
+nlemma union_is_ext_morph:∀A.𝛀^A ⇒_1 𝛀^A ⇒_1 𝛀^A.
+#A; napply (mk_binary_morphism1 … (union_is_ext …));
+#x1 x2 y1 y2 Ex Ey; napply (prop11 … (union_is_morph A)); nassumption.
+nqed.
+
+unification hint 1 ≔
+ AA : setoid, B,C : 𝛀^AA;
+ A ≟ carr AA,
+ R ≟ (mk_unary_morphism1 ??
+ (λS:𝛀^AA.
+ mk_unary_morphism1 ??
+ (λS':𝛀^AA.
+ mk_ext_powerclass AA (S ∪ S') (ext_prop AA (union_is_ext ? S S')))
+ (prop11 ?? (union_is_ext_morph AA S)))
+ (prop11 ?? (union_is_ext_morph AA))) ,
+ BB ≟ (ext_carr ? B),
+ CC ≟ (ext_carr ? C)
+(*------------------------------------------------------*) ⊢
+ ext_carr AA (R B C) ≡ union 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.
+
+nlemma test: ∀U.∀A,B:𝛀^U. A ∩ B = A →
+ ∀x,y. x=y → x ∈ A → y ∈ A ∩ B.
+ #U; #A; #B; #H; #x; #y; #K; #K2;
+ alias symbol "prop2" = "prop21 mem".
+ alias symbol "invert" = "setoid1 symmetry".
+ napply (. K^-1‡H);
+ nassumption;
+nqed.
+
+
+nlemma intersect_ok: ∀A. binary_morphism1 (ext_powerclass_setoid A) (ext_powerclass_setoid A) (ext_powerclass_setoid A).