How to create exhaustive print function for "enum" in Idris, off a string map

ExhaustivePrint.idr

%default total

data RPS = Rock | Paper | Scissors

Eq RPS where
  Rock == Rock = True
  Paper == Paper = True
  Scissors == Scissors = True
  _ == _ = False

StrMap : List (RPS, String)
StrMap =
  [ (Rock, "rock")
  , (Paper, "paper")
  , (Scissors, "scissors")
  ]

print' : RPS -> Maybe String
print' rps = lookup rps StrMap

print_exhaustive : (rps : RPS) -> IsJust (print' rps)
print_exhaustive Rock = ItIsJust
print_exhaustive Paper = ItIsJust
print_exhaustive Scissors = ItIsJust

justGetIt : (m : Maybe a) -> IsJust m -> a
justGetIt (Just y) ItIsJust = y

print : RPS -> String
print rps with (isItJust (print' rps))
  | Yes itIs = justGetIt (print' rps) itIs
  | No itsNot = absurd $ itsNot $ print_exhaustive rps