#A; @
[ napply (λS,S'. S ⊆ S' ∧ S' ⊆ S)
| /2/
- | #S; #S'; *; /2/
- | #S; #T; #U; *; #H1; #H2; *; /3/]
+ | #S; #S'; *; /3/
+ | #S; #T; #U; *; #H1; #H2; *; /4/]
nqed.
include "sets/setoids1.ma".
nlemma subseteq_is_morph: ∀A. unary_morphism1 (ext_powerclass_setoid A)
(unary_morphism1_setoid1 (ext_powerclass_setoid A) CPROP).
#A; napply (mk_binary_morphism1 … (λS,S':𝛀^A. S ⊆ S'));
- #a; #a'; #b; #b'; *; #H1; #H2; *; /4/.
+ #a; #a'; #b; #b'; *; #H1; #H2; *; /5/.
nqed.
unification hint 0 ≔ A,a,a'