def fail_done

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/kdf/proof.bend:29

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/kdf.bend as KDF
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

29def fail_done(+e: KDF.KdfError, +x: List<&2, U32>, +h: {Fail{e} == Done{x} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}) -> Empty:
30  L.false_true(Equal.cong(Result<&2, &2, KDF.KdfError, List<&2, U32>>, Bool, is_done, Fail{e}, Done{x}, h))