An alternative version of subtype.forall. This one is useful if Lean cannot figure out q when using subtype.forall from right to left.

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.