def tl.hl8_rs

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

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

7930def tl.hl8_rs() -> {List.length(&2, U32, GC.gc.rs.llist()) == A.Arrays.slots(8n) : Nat}:
7931  {==}