See Note [custom simps projection]
A version of x.property or x.2 where p is syntactically applied to the coercion of x
instead of x.1. A similar result is subtype.mem in data.set.basic.
An alternative version of subtype.forall. This one is useful if Lean cannot figure out q
when using subtype.forall from right to left.
Restrict a (dependent) function to a subtype
Defining a map into a subtype, this can be seen as an "coinduction principle" of subtype
Restriction of a function to a function on subtypes.
Some facts about sets, which require that α is a type.