∀ {m : Type w → Type w'} {α β : Type w} [inst : Std.Iterator α m β] {n : Type x → Type x'} [inst_1 : Monad n]
  (lift lift_1 : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ),
  lift = lift_1 →
    ∀ (γ : Type x) (PlausibleForInStep : β → γ → ForInStep γ → Prop) (it it_1 : Std.IterM m β) (e_it : it = it_1)
      (init init_1 : γ),
      init = init_1 →
        ∀ (P : β → Prop) (hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b)
          (f f_1 : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))),
          f = f_1 →
            Std.IterM.DefaultConsumers.forIn' lift γ PlausibleForInStep it init P hP f =
              Std.IterM.DefaultConsumers.forIn' lift_1 γ PlausibleForInStep it_1 init_1 P ⋯ f_1