law all_bytes_take

lawful-bytes@0.1.1.0 · proof_seq.bend:184

import Base
import lawful-bytes@0.1.1.0/defs.bend as D

184law all_bytes_take:
185  for +xs: List<&2, U32>
186  for +n: Nat
187  for +h: {D.all_bytes(xs) == True{} : Bool}
188  {D.all_bytes(List.take(&2, U32, xs, n)) == True{} : Bool}