PROOFOrder.wd.bool_flip: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF_order.bend as PROOFOrder
Lines 204-213 of bend-osdev-u32@0.1.0.0/PROOF_order.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF_order.bend&start_line=204&end_line=213

import Base

def wd.bool_flip(x: Bool, y: Bool) -> {Bool.cmp(y, x) == cm.flip(Bool.cmp(x, y)) : Cmp}:
  match x y:
    case False{} False{}:
      {==}
    case False{} True{}:
      {==}
    case True{} False{}:
      {==}
    case True{} True{}:
      {==}

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=Bool.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF_order.bend&name=cm.flip