law take_take

lawful-bytes@0.1.1.0 · proof_seq.bend:40

import Base

40law take_take:
41  for +xs: List<&2, U32>
42  for +m: Nat
43  for +n: Nat
44  for +h: {Nat.is_le(n, m) == True{} : Bool}
45  {List.take(&2, U32, List.take(&2, U32, xs, m), n) == List.take(&2, U32, xs, n) : List<&2, U32>}