law drop_length

lawful-bytes@0.1.1.0 · proof_shift.bend:38

import Base

38law drop_length:
39  for +xs: List<&2, U32>
40  for +k: Nat
41  {List.length(&2, U32, List.drop(&2, U32, xs, k)) == Nat.sub(List.length(&2, U32, xs), k) : Nat}