∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} {it : Std.IterM m β}
  {motive : (step : Std.IterStep (Std.IterM m β) β) → Std.Iterators.Types.TakeWhile.PlausibleStep it step → Prop}
  {step : Std.IterStep (Std.IterM m β) β} (t : Std.Iterators.Types.TakeWhile.PlausibleStep it step),
  (∀ {it' : Std.IterM m β} {out : β} (a : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out))
      (a_1 : (P out).Property { down := true }),
      motive (Std.IterStep.yield (Std.IterM.takeWhileWithPostcondition P it') out) ⋯) →
    (∀ {it' : Std.IterM m β} (a : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')),
        motive (Std.IterStep.skip (Std.IterM.takeWhileWithPostcondition P it')) ⋯) →
      (∀ (a : it.internalState.inner.IsPlausibleStep Std.IterStep.done), motive Std.IterStep.done ⋯) →
        (∀ {it' : Std.IterM m β} {out : β} (a : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out))
            (a_1 : (P out).Property { down := false }), motive Std.IterStep.done ⋯) →
          motive step t