∀ {α : Type u_1} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {b : Std.ExtTreeSet α cmp}
  (motive : (a : Std.ExtTreeSet α cmp) → (a == b) = true → Prop) (a : Std.ExtTreeSet α cmp) (hyp : (a == b) = true),
  (∀ (inner : Std.ExtDTreeMap α (fun x => Unit) cmp) (hyp : ({ inner := { inner := inner } } == b) = true),
      motive { inner := { inner := inner } } hyp) →
    motive a hyp