{α : Type} →
  {motive : Std.Bounded.State✝ α → Sort u} →
    ((producers : Std.Queue (IO.Promise Bool)) →
        (waiters : Std.Queue (Std.Broadcast.Consumer✝ α)) →
          (capacity : { x // 0 < x }) →
            (size : ℕ) →
              (buffer : Vector (IO.Ref (Std.Slot✝ α)) ↑capacity) →
                (write read : Fin ↑capacity) →
                  (receivers : Std.TreeMap ℕ ℕ compare) →
                    (nextId : ℕ) →
                      (closed : Bool) →
                        (pos : ℕ) →
                          motive
                            { producers := producers, waiters := waiters, capacity := capacity, size := size,
                              buffer := buffer, write := write, read := read, receivers := receivers, nextId := nextId,
                              closed := closed, pos := pos }) →
      (t : Std.Bounded.State✝¹ α) → motive t