{α : Type u_1} →
  {β : Type u_2} →
    (motive : Std.IterStep α β → Sort u_3) →
      (x : Std.IterStep α β) →
        ((it : α) → (out : β) → motive (Std.IterStep.yield it out)) →
          ((it : α) → motive (Std.IterStep.skip it)) → (Unit → motive Std.IterStep.done) → motive x