{α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Monad m] →
        [inst_1 : Std.Iterator α m β] →
          [Std.Iterators.Finite α m] →
            {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
              Std.Iterators.FinitenessRelation (Std.Iterators.Types.TakeWhile α m β P) m