law slice_snoc

lawful-bytes@0.1.1.0 · proof_same.bend:230

import Base
import lawful-bytes@0.1.1.0/defs.bend as D

230law slice_snoc:
231  for +xs: List<&2, U32>
232  for +i: Nat
233  for +k: Nat
234  for +x: U32
235  for +acc: List<&2, U32>
236  for +h: {List.get(&2, U32, xs, Nat.add(k, i)) == Some{x} : Maybe<&2, U32>}
237  {List.append(&2, U32, D.slice(xs, i, 1n+k), acc) == List.append(&2, U32, D.slice(xs, i, k), x <> acc) : List<&2, U32>}