- | #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #H
- [ napply (subseteq_trans … a)
- [ nassumption | napply (subseteq_trans … b); nassumption ]
- ##| napply (subseteq_trans … a')
- [ nassumption | napply (subseteq_trans … b'); nassumption ] ##]
+ | #a; #a'; #b; #b'; *; #Ha1; #Ha2; *;/4/]
+nqed.
+
+unification hint 0 ≔ A,a,a'
+ (*-----------------------------------------------------------------*) ⊢
+ eq_rel ? (eq A) a a' ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) a a'.
+
+nlemma intersect_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
+ #A; #S; #S'; @ (S ∩ S');
+ #a; #a'; #Ha; @; *; #H1; #H2; @
+ [##1,2: napply (. Ha^-1‡#); nassumption;
+##|##3,4: napply (. Ha‡#); nassumption]
+nqed.
+
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 0 ≔
+ A : setoid, B,C : ext_powerclass A;
+ R ≟ (mk_ext_powerclass ? (B ∩ C) (ext_prop ? (intersect_is_ext ? B C)))
+
+ (* ------------------------------------------*) ⊢
+ 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; *;/3/.
+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;