{α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        {P : β → Prop} →
          {motive : Std.Iterators.Types.Attach α m P → Sort u} →
            (t : Std.Iterators.Types.Attach α m P) →
              ((inner : Std.IterM m β) →
                  (invariant : ∀ (out : β), inner.IsPlausibleIndirectOutput out → P out) →
                    motive { inner := inner, invariant := invariant }) →
                motive t