-nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP.
- #A; napply mk_binary_morphism1
- [ napply (λS,S': qpowerclass_setoid ?. S ⊆ S')
- | #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; napply mk_iff; #H
- [ napply (subseteq_trans … a' a) (* anche qui, perche' serve a'? *)
- [ nassumption | napply (subseteq_trans … a b); nassumption ]
- ##| napply (subseteq_trans … a a') (* anche qui, perche' serve a'? *)
- [ nassumption | napply (subseteq_trans … a' b'); nassumption ] ##]
-nqed.
-
-nlemma intersect_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) (qpowerclass_setoid A).
- #A; napply mk_binary_morphism1
- [ #S; #S'; napply mk_qpowerclass
+ (* ------------------------------------------*) ⊢
+ ext_carr A R ≡ intersect ? (ext_carr ? B) (ext_carr ? C).
+
+nlemma intersect_is_morph:
+ ∀A. binary_morphism1 (powerclass_setoid A) (powerclass_setoid A) (powerclass_setoid A).
+ #A; @ (λS,S'. S ∩ S');
+ #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #x; nnormalize; *; #Ka; #Kb; @
+ [ napply Ha1; nassumption
+ | napply Hb1; nassumption
+ | napply Ha2; nassumption
+ | napply Hb2; nassumption]
+nqed.
+
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 0 ≔
+ A : Type[0], B,C : Ω^A;
+ R ≟ (mk_binary_morphism1 …
+ (λS,S'.S ∩ S')
+ (prop21 … (intersect_is_morph A)))
+ ⊢
+ fun21 (powerclass_setoid A) (powerclass_setoid A) (powerclass_setoid A) R B C
+ ≡ intersect ? B C.
+
+interpretation "prop21 ext" 'prop2 l r = (prop21 (ext_powerclass_setoid ?) (ext_powerclass_setoid ?) ? ? ???? l r).
+
+nlemma intersect_is_ext_morph:
+ ∀A. binary_morphism1 (ext_powerclass_setoid A) (ext_powerclass_setoid A) (ext_powerclass_setoid A).
+ #A; @ (intersect_is_ext …); nlapply (prop21 … (intersect_is_morph A));
+#H; #a; #a'; #b; #b'; #H1; #H2; napply H; nassumption;
+nqed.
+
+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.
+
+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).
+ #A; @
+ [ #S; #S'; @