PROOF.done_inj: def of bend-osdev-acpi@0.1.2.0
Import: import bend-osdev-acpi@0.1.2.0/PROOF.bend as PROOF
Lines 2344-2345 of bend-osdev-acpi@0.1.2.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/PROOF.bend&start_line=2344&end_line=2345

import Base
import bend-osdev-acpi@0.1.2.0/error.bend as E

def done_inj(-A: Data, +a: A, +b: A, +e: {Done{a} == Done{b} : Result<&2, &2, E.AcpiError, A>}) -> {a == b : A}:
  Equal.cong(Result<&2, &2, E.AcpiError, A>, A, x => Result.default(&2, &2, E.AcpiError, A, x, a), Done{a}, Done{b}, e)

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.default
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/error.bend&name=AcpiError