law pn

lawful-fields@0.1.1.0 · proof_cut.bend:336

import Base
import lawful-fields@0.1.1.0/defs.bend as F

336law pn:
337  for +es: List<&2, U32>
338  for +xs: List<&2, U32>
339  for +from: Nat
340  {F.pieces(es, xs, from) == PN(F.nats(es), xs, from) : List<&2, List<&2, U32>>}