{α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        {γ : Type x} →
          {PlausibleForInStep : β → γ → ForInStep γ → Prop} →
            {hwf : Std.IteratorLoop.WellFounded α m PlausibleForInStep} →
              Std.IterM m β → γ → Std.IteratorLoop.WithWF α m PlausibleForInStep hwf