exact Sublist.cons2 _ _ _ ih
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : (matchKey kvs k).snd <+ kvs
h : ¬kv.fst = k
⊢ (if False then (kv.snd :: (matchKey kvs k).fst, (matchKey kvs k).snd)
      else ((matchKey kvs k).fst, (kv.fst, kv.snd) :: (matchKey kvs k).snd)).snd <+
    kv :: kvs
no goals