def gt.elist_model

bend-osdev-gf@0.1.1.0 · proof_tab.bend:239

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

239def gt.elist_model(+f: G.Gf8Field) -> {gt.fe(510n, List.replicate(U32, A.Arrays.slots(9n), 0), f, 0n) == gt.elist(510n, f, 0n) : List<&2, U32>}:
240  {==}