{α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      {motive : Std.IterM m β → Sort u} →
        ((internalState : α) → motive { internalState := internalState }) → (t : Std.IterM m β) → motive t