simp only [matchKey, h, ite_true]
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : (matchKey kvs k).snd <+ kvs
h : kv.fst = k
⊢ (matchKey (kv :: kvs) k).snd <+ kv :: kvs
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : (matchKey kvs k).snd <+ kvs
h : kv.fst = k
⊢ (matchKey kvs k).snd <+ kv :: kvs