law final_extra_correct
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha/packed/packed_proof.bend:767
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/packed_proof.bend as PackedProof
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/packed/packed.bend as P
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha/packed.bend as R
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as S
767law final_extra_correct:
768 for +extra: Nat
769 for +more: Bool
770 for +total: Nat
771 for pair: Array<U32> & S.State
772 {P.final_extra(extra,more,total,pair) == R.final_extra(extra,more,total,pair) : Array<U32> & S.State}