Commit 2021-08-06 15:53 88f9480d
View on Github →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.