law tcons

lawful-bytes@0.1.1.0 · proof_fast_append.bend:44

import Base

44# A list whose first element is b.
45law tcons:
46  for +ys: List<&2, U32>
47  for +b: U32
48  for +m: Nat
49  for +rest: List<&2, U32>
50  for +h: {List.get(&2, U32, ys, 0n) == Some{b} : Maybe<&2, U32>}
51  for +ht: {List.take(&2, U32, List.drop(&2, U32, ys, 1n), m) == rest : List<&2, U32>}
52  {List.take(&2, U32, ys, 1n+m) == b <> rest : List<&2, U32>}