law drop_get

lawful-bytes@0.1.1.0 · proof_same.bend:49

import Base

49# Dropping j elements, when element j is x: x, then the rest.
50law drop_get:
51  for +xs: List<&2, U32>
52  for +j: Nat
53  for +x: U32
54  for +h: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>}
55  {List.drop(&2, U32, xs, j) == x <> List.drop(&2, U32, xs, Nat.add(j, 1n)) : List<&2, U32>}