law drop_cons

lawful-bytes@0.1.1.0 · proof_find.bend:48

import Base

48# Dropping j elements from a list with x at j leaves x in front.
49law drop_cons:
50  for +xs: List<&2, U32>
51  for +j: Nat
52  for +x: U32
53  for +hx: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>}
54  {List.drop(&2, U32, xs, j) == x <> List.drop(&2, U32, xs, Nat.add(j, 1n)) : List<&2, U32>}