law tg1

lawful-bytes@0.1.1.0 · proof_fast_append.bend:65

import Base

65# The first m (<= 4) elements of ys are b0 .. b3, given each one asked for.
66law tg1:
67  for +ys: List<&2, U32>
68  for +m: Nat
69  for +b0: U32
70  for +hm: {Nat.is_le(m, 1n) == True{} : Bool}
71  for g0: {Nat.is_lt(0n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 0n) == Some{b0} : Maybe<&2, U32>}
72  {List.take(&2, U32, ys, m) == List.take(&2, U32, [b0], m) : List<&2, U32>}