-unification hint 0 ≔
- A : Type[0], B,C : powerclass A ⊢
- fun21 …
- (mk_binary_morphism1 …
- (λS,S'.S ∩ S')
- (prop21 … (intersect_ok' A))) B C
- ≡ intersect ? B C.
-
-ndefinition prop21_mem :
- ∀A,C.∀f:binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) C.
- ∀a,a':setoid1_of_setoid A.
- ∀b,b':qpowerclass_setoid A.a = a' → b = b' → f a b = f a' b'.
-#A; #C; #f; #a; #a'; #b; #b'; #H1; #H2; napply prop21; nassumption;
+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.
+
+
+(* hints for - *)
+nlemma substract_is_morph : ∀A. Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A).
+#X; napply (mk_binary_morphism1 … (λA,B.A - B));
+#A1 A2 B1 B2 EA EB; napply ext_set; #x;
+nchange in match (x ∈ (A1 - B1)) with (?∧?);
+napply (.= (set_ext ??? EA x)‡#); @; *; #H H1; @; //; #H2; napply H1;
+##[ napply (. (set_ext ??? EB x)); ##| napply (. (set_ext ??? EB^-1 x)); ##] //;