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