def off.drop_drop

bend-osdev-bytes@0.1.1.0 · PROOF.bend:865

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

865def off.drop_drop(+j: Nat, +i: Nat, ws: List<&2, B.OctByte>) -> {B.w8s.drop(i, B.w8s.drop(j, ws)) == B.w8s.drop(Nat.add(j, i), ws) : List<&2, B.OctByte>}:
866  match j ws:
867    case 0n _:
868      {==}
869    case 1n+q Nil{}:
870      off.drop_nil(i)
871    case 1n+q Con{x, t}:
872      off.drop_drop(q, i, t)