∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] (it : Std.IterM m β)
  (acc : Array β),
  Std.IterM.toArray.go it acc =
    WellFounded.extrinsicFix₂ (InvImage Std.IterM.TerminationMeasures.Finite.Rel fun x => x.fst.finitelyManySteps!)
      (fun it acc recur => do
        let __do_lift ← it.step
        match __do_lift.inflate with
          | ⟨Std.IterStep.yield it' out, h⟩ => recur it' (acc.push out) ⋯
          | ⟨Std.IterStep.skip it', h⟩ => recur it' acc ⋯
          | ⟨Std.IterStep.done, property⟩ => pure acc)
      it acc