{m : Type u → Type u} →
  {motive : MLList.Spec✝ m → Sort u_1} →
    (t : MLList.Spec✝¹ m) →
      ((listM : Type u → Type u) →
          (nil : {α : Type u} → listM α) →
            (cons : {α : Type u} → α → listM α → listM α) →
              (thunk : {α : Type u} → (Unit → listM α) → listM α) →
                (squash : {α : Type u} → (Unit → m (listM α)) → listM α) →
                  (uncons : {α : Type u} → [Monad m] → listM α → m (Option (α × listM α))) →
                    (uncons? : {α : Type u} → listM α → Option (Option (α × listM α))) →
                      motive
                        { listM := listM, nil := nil, cons := cons, thunk := thunk, squash := squash, uncons := uncons,
                          uncons? := uncons? }) →
        motive t