law slice_length

lawful-bytes@0.1.1.0 · proof_fast_append.bend:234

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

234law slice_length:
235  for +xs: List<&2, U32>
236  for +s: Nat
237  for +a: Nat
238  for +h: {Nat.is_le(Nat.add(s, a), List.length(&2, U32, xs)) == True{} : Bool}
239  {List.length(&2, U32, D.slice(xs, s, a)) == a : Nat}