PROOF.Proof.forget_busy: def of bend-kube-runtime@0.2.0.0
Import: import bend-kube-runtime@0.2.0.0/PROOF.bend as PROOF
Lines 85-89 of bend-kube-runtime@0.2.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kube-runtime@0.2.0.0/PROOF.bend&start_line=85&end_line=89

import Base
import bend-kube-runtime@0.2.0.0/src/queue.bend as Q

# A busy key leaves any queue as it is.
def Proof.forget_busy(q: Q.Queue, key: String) -> {Q.Queue.forget.go(q, key, True{}) == q : Q.Queue}:
  match q:
    case Q.Queue{f, b, i, r, d, g, fl, n, mx}:
      {==}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/queue.bend&name=Queue
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/queue.bend&name=Queue.forget.go