-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).
+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).