∀ {m : Type w → Type w'} {α₁ β₁ : Type w} [inst : Std.Iterator α₁ m β₁] {α₂ β₂ : Type w} [inst_1 : Std.Iterator α₂ m β₂]
  {it : Std.IterM m (β₁ × β₂)}
  {motive : (a : Std.IterStep (Std.IterM m (β₁ × β₂)) (β₁ × β₂)) → Std.Iterators.Types.Zip.PlausibleStep it a → Prop},
  (∀ (hm : it.internalState.memoizedLeft = none) {it' : Std.IterM m β₁} {out : β₁}
      (hp : it.internalState.left.IsPlausibleStep (Std.IterStep.yield it' out)),
      motive
        (Std.IterStep.skip
          { internalState := { left := it', memoizedLeft := some ⟨out, ⋯⟩, right := it.internalState.right } })
        ⋯) →
    (∀ (hm : it.internalState.memoizedLeft = none) {it' : Std.IterM m β₁}
        (hp : it.internalState.left.IsPlausibleStep (Std.IterStep.skip it')),
        motive
          (Std.IterStep.skip
            { internalState := { left := it', memoizedLeft := none, right := it.internalState.right } })
          ⋯) →
      (∀ (hm : it.internalState.memoizedLeft = none) (hp : it.internalState.left.IsPlausibleStep Std.IterStep.done),
          motive Std.IterStep.done ⋯) →
        (∀ {out₁ : { out // ∃ it, it.IsPlausibleOutput out }} (hm : it.internalState.memoizedLeft = some out₁)
            {it₂' : Std.IterM m β₂} {out₂ : β₂}
            (hp : it.internalState.right.IsPlausibleStep (Std.IterStep.yield it₂' out₂)),
            motive
              (Std.IterStep.yield
                { internalState := { left := it.internalState.left, memoizedLeft := none, right := it₂' } }
                (↑out₁, out₂))
              ⋯) →
          (∀ {out₁ : { out // ∃ it, it.IsPlausibleOutput out }} (hm : it.internalState.memoizedLeft = some out₁)
              {it₂' : Std.IterM m β₂} (hp : it.internalState.right.IsPlausibleStep (Std.IterStep.skip it₂')),
              motive
                (Std.IterStep.skip
                  { internalState := { left := it.internalState.left, memoizedLeft := some out₁, right := it₂' } })
                ⋯) →
            (∀ {out₁ : { out // ∃ it, it.IsPlausibleOutput out }} (hm : it.internalState.memoizedLeft = some out₁)
                (hp : it.internalState.right.IsPlausibleStep Std.IterStep.done), motive Std.IterStep.done ⋯) →
              ∀ {a : Std.IterStep (Std.IterM m (β₁ × β₂)) (β₁ × β₂)} (t : Std.Iterators.Types.Zip.PlausibleStep it a),
                motive a t