refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
-- Like refineType, but returns the 'sym' coercion
-- If (refineResType r ty) = (co, ty')
refineResType :: Refinement -> Type -> Maybe (Coercion, Type)
-- Like refineType, but returns the 'sym' coercion
-- If (refineResType r ty) = (co, ty')