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'));
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'));