def key_succ

bend-kit-scheduler@0.4.1.0 · queue_proof.bend:44

import Base
import bend-kit-scheduler@0.4.1.0/queue.bend as Q

44def key_succ(b: Bool, i: Nat, j: Nat, d: Nat, e: Nat) -> {Q.le.same(b, i, j, 1n+d, 1n+e) == Q.le.same(b, i, j, d, e) : Bool}:
45  match b:
46    case True{}:
47      {==}
48    case False{}:
49      {==}