LAWS.bind_cong: law of bend-osdev-mode-core@0.1.0.0
Import: import bend-osdev-mode-core@0.1.0.0/LAWS.bend as LAWS
Lines 157-163 of bend-osdev-mode-core@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&start_line=157&end_line=163

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M

# a bind whose continuations agree on every value agrees
law bind_cong:
  for r: Result<&2, &2, M.CmError, B.Octets>
  for f: B.Octets -> Result<&2, &2, M.CmError, B.Octets>
  for g: B.Octets -> Result<&2, &2, M.CmError, B.Octets>
  for h: @c: B.Octets -> {f(c) == g(c) : Result<&2, &2, M.CmError, B.Octets>}
  {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, f) == Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, r, g) : Result<&2, &2, M.CmError, B.Octets>}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.bind
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=tr.bind_cong
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=CmError