subtype to type

Stream: Is there code for X?

[Kayla Thomas]

Is there an easy one size fits all way to convert a list of subtypes to a list of the type they are a subtype of, a function from subtypes to subtypes to a function from types to types, etc.?

[Kayla Thomas]

Not as a tactic, but in statements of theorems.

[Mario Carneiro]

no, specifically you can't go from a function from subtypes to subtypes to a function from types to types

[Mario Carneiro]

because the subtype function may require the subtype property to generate the output value

[Kayla Thomas]

I see. Ok.

[Kayla Thomas]

Thank you.