{α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {motive : Std.ExtTreeMap α β cmp → Sort u_1} →
        (t : Std.ExtTreeMap α β cmp) →
          ((inner : Std.ExtDTreeMap α (fun x => β) cmp) → motive { inner := inner }) → motive t