law get_word_ok
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/cipher.bend:279
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher.bend as Cipher
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/aes.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S
279law get_word_ok:
280 for +ws: List<&2, T.Quad>
281 for +n: Nat
282 {I.get_word(ws, n) == S.nth_word(ws, n) : T.Quad}