{α α₂ β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m (Std.IterM m β)] →
      (it₁ : Std.IterM m (Std.IterM m β)) →
        (motive : it₁.Step → Sort u_3) →
          (x : it₁.Step) →
            ((it₁' : Std.IterM m (Std.IterM m β)) →
                (it₂' : Std.IterM m β) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' it₂')) → motive ⟨Std.IterStep.yield it₁' it₂', h⟩) →
              ((it₁' : Std.IterM m (Std.IterM m β)) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩) →
                ((h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x