law pieces_length

lawful-fields@0.1.1.0 · proof_list.bend:425

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

425law pieces_length:
426  for +es: List<&2, U32>
427  for +xs: List<&2, U32>
428  for +from: Nat
429  {List.length(&2, List<&2, U32>, F.pieces(es, xs, from)) == List.length(&2, U32, es) : Nat}