law take_length

lawful-bytes@0.1.1.0 · proof_seq.bend:22

import Base

22law take_length:
23  for +xs: List<&2, U32>
24  for +n: Nat
25  for +h: {Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool}
26  {List.length(&2, U32, List.take(&2, U32, xs, n)) == n : Nat}