def done_cong

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/kdf.bend as KDF

35def done_cong(+x: List<&2, U32>, +y: List<&2, U32>, +h: {x == y : List<&2, U32>}) -> {Done{x} == Done{y} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}:
36  %h : {Done{x} == Done{_} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
37  {==}