law get_drop

lawful-bytes@0.1.1.0 · proof_same.bend:192

import Base

192law get_drop:
193  for +xs: List<&2, U32>
194  for +i: Nat
195  for +k: Nat
196  {List.get(&2, U32, List.drop(&2, U32, xs, i), k) == List.get(&2, U32, xs, Nat.add(i, k)) : Maybe<&2, U32>}