Ah, I see. If you view functors as being checked once, then the fact that there exists, for each arm of the case, a structure you could apply the functor to which would result in that arm being the one followed is enough. f