∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] [inst_2 : DenselyOrdered α]
  [inst_3 : NoMinOrder α] [inst_4 : NoMaxOrder α] [inst_5 : Nonempty α] (b : β) (I : Order.Ideal (Order.PartialIso α β))
  (motive : (∃ f ∈ Order.PartialIso.definedAtRight α b, f ∈ I) → Prop)
  (x : ∃ f ∈ Order.PartialIso.definedAtRight α b, f ∈ I),
  (∀ (f : Order.PartialIso α β) (a : α) (ha : (a, b) ∈ ↑f) (hf : f ∈ I), motive ⋯) → motive x