∀ {α β : Type u_1} {m : Type u_1 → Type u_3} {n : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  {f : β → Std.Iterators.PostconditionT n (ULift.{u_1, 0} Bool)} [inst_1 : Monad n] [inst_2 : MonadLiftT m n]
  (it' : Std.IterM m β) (out : β),
  it.IsPlausibleStep (Std.IterStep.yield it' out) →
    (f out).Property { down := true } →
      (Std.IterM.filterWithPostcondition f it).IsPlausibleStep
        (Std.IterStep.yield (Std.IterM.filterWithPostcondition f it') out)