law slice_cons

lawful-bytes@0.1.1.0 · proof_append.bend:92

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

92# A slice of 1 + k from i starts with element i.
93law slice_cons:
94  for +xs: List<&2, U32>
95  for +i: Nat
96  for +k: Nat
97  for +x: U32
98  for +h: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
99  {D.slice(xs, i, 1n+k) == x <> D.slice(xs, Nat.add(i, 1n), k) : List<&2, U32>}