∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  {n : Type u_1 → Type u_3} (γ : Type u_1) (Pl : α → γ → ForInStep γ → Prop)
  (motive :
    (it : Std.IterM Id α) → ((b : α) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) → Sort u_2)
  (next upperBound : α)
  (f :
    (b : α) →
      { internalState := { next := some next, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
        (c : γ) → n (Subtype (Pl b c)))
  (h_1 :
    (next upperBound : α) →
      (f :
          (b : α) →
            { internalState := { next := some next, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
              (c : γ) → n (Subtype (Pl b c))) →
        motive { internalState := { next := some next, upperBound := upperBound } } f)
  (h_2 :
    (upperBound : α) →
      (f :
          (b : α) →
            { internalState := { next := none, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
              (c : γ) → n (Subtype (Pl b c))) →
        motive { internalState := { next := none, upperBound := upperBound } } f),
  (match { internalState := { next := some next, upperBound := upperBound } }, f with
    | { internalState := { next := some next, upperBound := upperBound } }, f => h_1 next upperBound f
    | { internalState := { next := none, upperBound := upperBound } }, f => h_2 upperBound f) =
    h_1 next upperBound f