∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (fallback : (a : α) × β a) (x : List ((a : α) × β a)),
  Std.Internal.List.getEntryD a fallback x =
    match x with
    | [] => fallback
    | ⟨k, v⟩ :: l => bif k == a then ⟨k, v⟩ else Std.Internal.List.getEntryD a fallback l