∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (l l_1 : List ((a : α) × β a)),
  l = l_1 →
    ∀ (fallback fallback_1 : β a),
      fallback = fallback_1 →
        Std.Internal.List.getValueCastD a l fallback = Std.Internal.List.getValueCastD a l_1 fallback_1