∀ {α : Type u_1} [inst : CompleteLattice α] (f : α →o α)
  (motive : (∃ y, OrdinalApprox.lfpApprox f ⊥ (Order.succ (Cardinal.mk α)).ord = ↑y) → Prop)
  (h_fix : ∃ y, OrdinalApprox.lfpApprox f ⊥ (Order.succ (Cardinal.mk α)).ord = ↑y),
  (∀ (x : ↑(Function.fixedPoints ⇑f)) (h_x : OrdinalApprox.lfpApprox f ⊥ (Order.succ (Cardinal.mk α)).ord = ↑x),
      motive ⋯) →
    motive h_fix