law take_snoc

lawful-bytes@0.1.1.0 · proof_shift.bend:70

import Base

70law take_snoc:
71  for +ys: List<&2, U32>
72  for +j: Nat
73  for +x: U32
74  for +h: {List.get(&2, U32, ys, j) == Some{x} : Maybe<&2, U32>}
75  {List.take(&2, U32, ys, Nat.add(j, 1n)) == List.append(&2, U32, List.take(&2, U32, ys, j), [x]) : List<&2, U32>}