law slice_cons

lawful-bytes@0.1.1.0 · proof_find.bend:68

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

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