law drop_set0

lawful-bytes@0.1.1.0 · proof_shift.bend:52

import Base

52# Setting the first element of drop(xs, j).
53law drop_set0:
54  for +xs: List<&2, U32>
55  for +j: Nat
56  for +x: U32
57  for +h: {Nat.is_lt(j, List.length(&2, U32, xs)) == True{} : Bool}
58  {List.set(&2, U32, List.drop(&2, U32, xs, j), 0n, x) == x <> List.drop(&2, U32, xs, Nat.add(j, 1n)) : List<&2, U32>}