def tl.hl8_aes

bend-osdev-gf@0.1.1.0 · PROOF.bend:7913

import Base
import bend-osdev-array@0.1.0.1/array.bend as A
import bend-osdev-gf@0.1.1.0/proof_tab_cases.bend as GC

7913def tl.hl8_aes() -> {List.length(&2, U32, GC.gc.aes.llist()) == A.Arrays.slots(8n) : Nat}:
7914  {==}