∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {a : α}
  (h : Std.Internal.List.containsKey a l = true),
  some (Std.Internal.List.getValue a l h) = Std.Internal.List.getValue? a l