The above just test for existence, but a slight modification, based on the same logical expression, gets us to a winning strategy:

     -- Game data
     data Player = P1 | P2
            deriving (Eq, Show)

     data Color = Red | Blue
            deriving (Eq, Show)

     data State = S [Color]
            deriving (Eq, Show)

     data Strategy = Won
                   | Force Color Strategy
                   | Choice (Color -> Strategy)



    -- Modal operators
    e' = modal sany' (Coalg possible')
    a' = modal sall' (Coalg possible')

     -- Test for winning strategy within a limited number of moves.
     winning' :: Integer -> Player -> State -> Maybe Strategy
     winning' 0 _ _ = Nothing
     winning' n p s = wonAlready <|> (e' (a' (winning' (n-1) p)) s) where
            wonAlready = if (winner s == Just p) then Just Won else Nothing