{α : Type u_6} →
  {motive : OmegaCompletePartialOrder α → Sort u} →
    (t : OmegaCompletePartialOrder α) →
      ([toPartialOrder : PartialOrder α] →
          (ωSup : OmegaCompletePartialOrder.Chain α → α) →
            (le_ωSup : ∀ (c : OmegaCompletePartialOrder.Chain α) (i : ℕ), c i ≤ ωSup c) →
              (ωSup_le : ∀ (c : OmegaCompletePartialOrder.Chain α) (x : α), (∀ (i : ℕ), c i ≤ x) → ωSup c ≤ x) →
                motive { toPartialOrder := toPartialOrder, ωSup := ωSup, le_ωSup := le_ωSup, ωSup_le := ωSup_le }) →
        motive t