{α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {m₁ m₂ : Std.TreeMap.Raw α β cmp} →
        {motive : m₁.Equiv m₂ → Sort u_1} →
          (t : m₁.Equiv m₂) → ((inner : m₁.inner.Equiv m₂.inner) → motive ⋯) → motive t