def done_inj

bend-osdev-acpi@0.1.1.0 · PROOF.bend:2344

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

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