Magic pattern-matching on `Elem`

ElemSplit.idr

import Data.String
import Data.List
import Data.List.Elem
import Decidable.Decidable
import Decidable.Equality

%default total

toWitness : (prf1 : Dec a) -> IsYes prf1 -> a
toWitness (Yes prf2) x = prf2

fromString : (k : String) ->
             {ks : List String} ->
             IsYes (k `isElem` ks) =>
             k `Elem` ks
fromString k @{p} = toWitness _ p

Example : List String
Example = ["0", "1", "2"]

mycase : {0 s : String} -> s `Elem` Example -> Nat
mycase "0" = 0
mycase "1" = 1
mycase "2" = 2