∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {ps : Std.Do.PostShape} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)}
  {inv : Std.Do.PostCond β ps},
  (∀ (x : α) (hx : x ∈ xs) (b : β),
      ⦃inv.1 b⦄
        f x hx b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 b'
          | ForInStep.done b' => inv.1 b',
          inv.2)⦄) →
    ⦃inv.1 init⦄ forIn' xs init f ⦃inv⦄