{α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {γ : Type u_1} →
        {δ : Type u_2} → (α → β → γ → δ) → Batteries.RBMap α β cmp → Batteries.RBMap α γ cmp → Batteries.RBMap α δ cmp