That's exactly what my framework does. As long as you're okay with runtime panics (which would happen anyway in a non-dependently typed language), you just have any function you don't know how to prove go from SortedList -> List. Then you have a check List -> Maybe SortedList. And finally a function with a panic that lets you write the SortedList -> SortedList version.