{α : Type u_1} →
  {cmp : α → α → Ordering} →
    {β : Type u_2} →
      {t : Std.ExtDTreeMap α (fun x => β) cmp} →
        [inst : Std.TransCmp cmp] →
          (motive : { x // x ∈ t.keys } → Sort u_3) →
            (x : { x // x ∈ t.keys }) → ((x : α) → (h' : x ∈ t.keys) → motive ⟨x, h'⟩) → motive x