∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α}
  {f : β → Std.Iterators.PostconditionT n (Option γ)} [inst : Std.Iterator α m β] {it : Std.IterM n γ}
  {it' : Std.IterM m β} {out : β} {out' : γ},
  it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out) →
    (f out).Property (some out') →
      Std.Iterators.Types.FilterMap.PlausibleStep it
        (Std.IterStep.yield (Std.IterM.InternalCombinators.filterMap lift f it') out')