law slice_cons

lawful-bytes@0.1.1.0 · proof_same.bend:70

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

70law slice_cons:
71  for +xs: List<&2, U32>
72  for +j: Nat
73  for +k: Nat
74  for +x: U32
75  for +h: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>}
76  {D.slice(xs, j, 1n+k) == x <> D.slice(xs, Nat.add(j, 1n), k) : List<&2, U32>}