law at_drop

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

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

437law at_drop:
438  for +j: Nat
439  for +xs: List<&2, U32>
440  for +i: Nat
441  {B.at(B.drop(j, xs), i) == B.at(xs, Nat.add(j, i)) : Maybe<&2, U32>}