law at_append_add

bend-osdev-bytes@0.1.1.0 · LAWS.bend:424

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

424law at_append_add:
425  for +a: List<&2, U32>
426  for +b: List<&2, U32>
427  for +i: Nat
428  {B.at(B.append(a, b), Nat.add(B.len(a), i)) == B.at(b, i) : Maybe<&2, U32>}