∀ {m : Type w → Type x} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] {γ : Type u}
  {α β : Type w} [LawfulMonad m] {δ : Type w} [inst_3 : Std.ToIterator (Std.Slice γ) Id α β]
  [inst_4 : Std.Iterator α Id β] [inst_5 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m]
  [Std.Iterators.Finite α Id] {init : δ} {f : β → δ → m (ForInStep δ)} {xs : Std.Slice γ}
  (inv : Std.Do.Invariant xs.toList δ ps),
  (∀ (pref : List β) (cur : β) (suff : List β) (h : xs.toList = pref ++ cur :: suff) (b : δ),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄