∀ {α : Type u_1} {β : α → Type u_2} {cmp : α → α → Ordering} {t₁ : Std.DTreeMap α β cmp} {k : α} (x : α)
  (motive : x ∈ t₁ ∧ (cmp x k).isLE = true → Prop) (x_1 : x ∈ t₁ ∧ (cmp x k).isLE = true),
  (∀ (h₁ : x ∈ t₁) (h₂ : (cmp x k).isLE = true), motive ⋯) → motive x_1