Key-value mapping in Idris where set of keys that have values is encoded in the type

SetMap.idr

import Data.List

data SetMap : List k -> Type -> Type where
  Empty : SetMap [] _
  Insert : DecEq k =>
           (key : k) ->
           v ->
           SetMap keys v ->
           {auto prf : isElem key keys = No _} ->
           SetMap (key :: keys) v

example : SetMap ["a", "b"] Nat
example = Insert "a" 2 $
          Insert "b" 1 $
          Empty