feat(logic/embedding): subtype_or_{embedding,equiv} (#8489)
Provide explicit embedding from a subtype of a disjuction into a sum type.
If the disjunction is disjoint, upgrade to an equiv.
Additionally, provide `subtype.imp_embedding`, lowering a subtype
along an implication.
