def next_words_16
import qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend as AESNistKeyScheduleProofimport Base
import qasim-bend-kit@0.1.0.2/proof/AES_TraceProof.bend as Trace
233def next_words_16() ->
234 {List.append(&2, U32, words_16(), [Trace.next_word(16, 2, words_16())]) == words_17() : List<&2, U32>}:
235 {==}