{α : Type u_1} →
  [inst : Preorder α] →
    {motive : ClosureOperator α → Sort u} →
      (t : ClosureOperator α) →
        ((toOrderHom : α →o α) →
            (le_closure' : ∀ (x : α), x ≤ toOrderHom.toFun x) →
              (idempotent' : ∀ (x : α), toOrderHom.toFun (toOrderHom.toFun x) = toOrderHom.toFun x) →
                (IsClosed : α → Prop) →
                  (isClosed_iff : ∀ {x : α}, IsClosed x ↔ toOrderHom.toFun x = x) →
                    motive
                      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent',
                        IsClosed := IsClosed, isClosed_iff := isClosed_iff }) →
          motive t