In my last post I described a style which uses Subtype as a return type in order to merge the primary theorem about a function with its type signature. If I use this style for my own code, my functions will take inputs of some arbitrary types, but always return a Subtype as a final result. And when writing new code I will want to combine such functions by applying one to the result of another. More precisely, given a value of type Subtype p_α, with p_α : α → Prop, and a function f : α → Subtype p_β , with p_β : β → Prop, I want to get a result of type Subtype p_β‘, for some suitable[…]