law schedule_correct
import bend-collections@1.0.0.0/proofs/crypto/sha/packed/conformance.bend as Conformanceimport Base
import bend-collections@1.0.0.0/proofs/crypto/sha/packed/core_model.bend as C
import bend-collections@1.0.0.0/spec/crypto/sha.bend as F
102law schedule_correct:
103 for +extra: Nat
104 for +block: List<&2, U32>
105 {C.schedule(extra, block) == F.schedule(extra, block) : List<&2, U32>}