∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
  {h : Std.Internal.List.containsKey a (Std.Internal.List.eraseKey k l) = true} (hl : Std.Internal.List.DistinctKeys l),
  Std.Internal.List.getValueCast a (Std.Internal.List.eraseKey k l) h = Std.Internal.List.getValueCast a l ⋯