∀ {m : Type w → Type w'} {α β : Type w} [inst : Std.Iterator α m β] {n : Type x → Type x'} [inst_1 : Monad n]
  (lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x)
  (PlausibleForInStep : β → γ → ForInStep γ → Prop) (wf : Std.IteratorLoop.WellFounded α m PlausibleForInStep)
  (P : β → Prop) (f : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c)))
  (_x : (it : Std.IterM m β) ×' (_ : γ) ×' ∀ (b : β), it.IsPlausibleIndirectOutput b → P b),
  Std.IterM.DefaultConsumers.forIn'.wf._unary lift γ PlausibleForInStep wf P f _x =
    PSigma.casesOn _x fun it init =>
      PSigma.casesOn init fun init hP =>
        (fun x => lift (Std.Shrink it.Step) γ x it.step) fun s =>
          match s.inflate with
          | ⟨Std.IterStep.yield it' out, h⟩ => do
            let __do_lift ← f out ⋯ init
            match __do_lift with
              | ⟨ForInStep.yield c, property⟩ =>
                Std.IterM.DefaultConsumers.forIn'.wf._unary lift γ PlausibleForInStep wf P f ⟨it', ⟨c, ⋯⟩⟩
              | ⟨ForInStep.done c, property⟩ => pure c
          | ⟨Std.IterStep.skip it', h⟩ =>
            Std.IterM.DefaultConsumers.forIn'.wf._unary lift γ PlausibleForInStep wf P f ⟨it', ⟨init, ⋯⟩⟩
          | ⟨Std.IterStep.done, property⟩ => pure init