∀ {α β γ : 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 γ}
  {motive : (a : Std.IterStep (Std.IterM n γ) γ) → Std.Iterators.Types.FilterMap.PlausibleStep it a → Prop},
  (∀ {it' : Std.IterM m β} {out : β} (a : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out))
      (a_1 : (f out).Property none),
      motive (Std.IterStep.skip (Std.IterM.InternalCombinators.filterMap lift f it')) ⋯) →
    (∀ {it' : Std.IterM m β} {out : β} {out' : γ}
        (a : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) (a_1 : (f out).Property (some out')),
        motive (Std.IterStep.yield (Std.IterM.InternalCombinators.filterMap lift f it') out') ⋯) →
      (∀ {it' : Std.IterM m β} (a : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')),
          motive (Std.IterStep.skip (Std.IterM.InternalCombinators.filterMap lift f it')) ⋯) →
        (∀ (a : it.internalState.inner.IsPlausibleStep Std.IterStep.done), motive Std.IterStep.done ⋯) →
          ∀ {a : Std.IterStep (Std.IterM n γ) γ} (t : Std.Iterators.Types.FilterMap.PlausibleStep it a), motive a t