{α β : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      {n : Type x → Type x'} →
        [Monad n] →
          {P : β → Prop} → [inst_2 : Std.Iterator α m β] → Std.IteratorLoop (Std.Iterators.Types.Attach α m P) m n