- (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;
-nqed.
-
-interpretation "prop21 mem" 'prop2 l r = (prop21_mem ??????? l r).
-
-nlemma intersect_ok'':
- ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) (qpowerclass_setoid A).
- #A; @ (intersect_ok A); nlapply (prop21 … (intersect_ok' A)); #H;
- #a; #a'; #b; #b'; #H1; #H2; napply H; nassumption;
+ (prop21 … (intersect_is_morph A)))
+ ⊢
+ fun21 (powerclass_setoid A) (powerclass_setoid A) (powerclass_setoid A) R B C
+ ≡ intersect ? B C.
+
+interpretation "prop21 mem" 'prop2 l r = (prop21 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ???? l r).
+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;