law take_snoc

lawful-bytes@0.1.1.0 · proof_same.bend:207

import Base

207# Taking k + 1 elements then acc is taking k then element k, then acc.
208law take_snoc:
209  for +ys: List<&2, U32>
210  for +k: Nat
211  for +x: U32
212  for +acc: List<&2, U32>
213  for +h: {List.get(&2, U32, ys, k) == Some{x} : Maybe<&2, U32>}
214  {List.append(&2, U32, List.take(&2, U32, ys, 1n+k), acc) == List.append(&2, U32, List.take(&2, U32, ys, k), x <> acc) : List<&2, U32>}