-unification hint 1 ≔
- A : setoid, B,C : qpowerclass A ⊢
- pc A (mk_qpowerclass ? (B ∩ C) (mem_ok' ? (intersect_ok ? B C)))
- ≡ intersect ? (pc ? B) (pc ? C).
-
-unification hint 1 ≔
- A : setoid, B,C : qpowerclass A;
- DX ≟ (intersect ? (pc ? B) (pc ? C)),
- SX ≟ (mk_qpowerclass ? (B ∩ C) (mem_ok' ? (intersect_ok ? B C)))
- (*-----------------------------------------------------------------*) ⊢
- pc A SX ≡ DX.
-
-nlemma intersect_ok': ∀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]
+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. unary_morphism1 (powerclass_setoid A) (unary_morphism1_setoid1 (powerclass_setoid A) (powerclass_setoid A)).
+ #A; napply (mk_binary_morphism1 … (λS,S'. S ∩ S'));
+ #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #x; nnormalize; *;/3/.