{m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    (motive : Std.IterM m α → Sort u_3) →
      (it : Std.IterM m α) →
        (Unit → motive { internalState := { list := [] } }) →
          ((x : α) → (xs : List α) → motive { internalState := { list := x :: xs } }) → motive it