∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {p : (a : α) × β a}
  {k : α} {h₁ : Std.Internal.List.containsKey k l = true}, Std.Internal.List.getEntry k l h₁ = p → (p.fst == k) = true